Lecture: Software Analysis and Verification


This course covers advanced techniques for automatic software verification, especially techniques belonging to the field of program analysis or software model checking. The course continues the bachelor course Formal Verification and Specification 1 (FSV 1). Knowledge from FSV 1 is helpful, but not mandatory. The following list provides on overview of topics covered by the course:



Please register for this course at the new Uni2work.


Lecture: Di 14:15-15:45 Uhr, Amalienstr. 73A, 220 First Lecture: 15.10.2019
Tutorial: Do 14:15-15:45 Uhr, Ludwigstr. 28, RG, 024 First Tutorial: 24.10.2019


Master Computer Science (Master Informatik)


Die folgenden Materialien unterliegen dem Copyright. Teilnehmern der Vorlesung ist die Verwendung für persönliche Studien gestattet. Alle anderen Rechte sind vorbehalten.
English Translation The following material is subject to copyright. Participants of the course are granted to use the material for personal studies only. All rights are reserved.

User name and password will be announced in the lecture and the tutorial. If the new Uni2work system works for uploading lecture material, we might also upload the material there.

Lecture Slides

Complete slide deck up to current lecture progress: swav.pdf
Introduction,Program Syntax
22019-10-22Concrete semantics,
Abstract Domains, Abstract semantics
32019-10-29Example domainsswav03.pdf
42019-11-07Flow-insensitive analysisswav04.pdf
52019-11-19Dataflow analysisswav05.pdf
62019-12-03Model Checkingswav06.pdf
72019-12-10Configurable Program Analysiscf. swav06.pdf
82020-01-07Abstract Reachability Graph
Counterexample-guided abstraction refinement
92020-01-28Lazy abstractionexternal slides


DateSheetExample SolutionComments
22019-10-31sheet02.pdfsheet02-solution.pdf Update (2019-11-03): Fixed two errors in solution
32019-11-07sheet03.pdfsheet03-solution.pdf Update (2019-11-19): Fixed errors in sheet and solution(found during tutorial)
2019-11-14no sheetno tutorial
42019-11-21sheet04.pdfsheet04-solution.pdf Still missing some parts of solution
52019-11-28 Q&A Session
62019-12-05sheet05.pdf sheet05-solution.pdfBeware of known bugs in the solution that are not yet fixed



to be continued
  1. Nielson, Flemming, Hanne R. Nielson, and Chris Hankin. Principles of program analysis. Springer, 1999
  2. Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, Roderick Bloem (Eds.). Handbook of Model Checking. Springer, 2018.

  3. Vijay D'Silva, Daniel Kroening, Georg Weissenbacher. A Survey of Automated Techniques for Formal Software Verification. IEEE Trans. on CAD of Integrated Circuits and Systems 27(7), IEEE, 2008
  4. Ranjit Jhala and Rupak Majumdar. Software model checking. ACM Comput. Surv. 41(4), Article 21, ACM, 2009.

  5. Dirk Beyer, Thomas A. Henzinger, GrégoryThéoduloz. Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis. CAV 2007, Lecture Notes in Computer Science, vol 4590, Springer, 2009.
  6. Dirk Beyer, Stefan Löwe, Philipp Wendler. Sliced Path Prefixes: An Effective Method to Enable Refinement Selection. FORTE 2015, Lecture Notes in Computer Science, vol 9039, Springer, 2015.
  7. Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu, Roberto Sebastiani. Software model checking via large-block encoding. FMCAD 2009, IEEE, 2009.
  8. Matthias Heizmann, Jochen Hoenicke, Andreas Podelski. Refinement of Trace Abstraction. SAS 2009, Lecture Notes in Computer Science, vol 5673, Springer, 2009.

  9. Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Ofer Strichman, Yunshan Zhu. Bounded Model Checking. Advances in Computers, vol 58, Elsevier, 2003.
  10. Edmund Clarke, Daniel Kroening, and Karen Yorav. Behavioral consistency of C and Verilog programs using bounded model checking. DAC 2003, ACM, 2003.