Lecture: Software Analysis and Verification

Content

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:

• Flow-insensitive analysis
• Dataflow analysis and abstract interpretation
• Explicit and abstract model checking
  • Counterexample guided abstraction refinement
  • Lazy abstraction
  • Interpolation
• SAT-based model checking

Organization

• Lecturer: Prof. Dr. Dirk Beyer
• Assistants: Stephan Holzner, Martin Spießl

Registration

Please register for this course at the new Uni2work.

Dates

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

Audience

Master Computer Science (Master Informatik)

Material

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

	Date	Topics	Slides
1	2019-10-15	Organisation, Introduction,Program Syntax	swav01.pdf
2	2019-10-22	Concrete semantics, Abstract Domains, Abstract semantics	swav02.pdf
3	2019-10-29	Example domains	swav03.pdf
4	2019-11-07	Flow-insensitive analysis	swav04.pdf
5	2019-11-19	Dataflow analysis	swav05.pdf
6	2019-12-03	Model Checking	swav06.pdf
7	2019-12-10	Configurable Program Analysis	cf. swav06.pdf
8	2020-01-07	Abstract Reachability Graph Counterexample-guided abstraction refinement	swav07.pdf
9	2020-01-28	Lazy abstraction	external slides

Exercises

	Date	Sheet	Example Solution	Comments
1	2019-10-24	sheet01.pdf	sheet01-solution.pdf
2	2019-10-31	sheet02.pdf	sheet02-solution.pdf	Update (2019-11-03): Fixed two errors in solution
3	2019-11-07	sheet03.pdf	sheet03-solution.pdf	Update (2019-11-19): Fixed errors in sheet and solution(found during tutorial)
	2019-11-14	no sheet	no tutorial
4	2019-11-21	sheet04.pdf	sheet04-solution.pdf	Still missing some parts of solution
5	2019-11-28			Q&A Session
6	2019-12-05	sheet05.pdf	sheet05-solution.pdf	Beware of known bugs in the solution that are not yet fixed
7	2019-12-12	sheet06.pdf	sheet06-solution.pdf
8	2019-12-19	sheet07.pdf	sheet07-solution.pdf
9	2020-01-09
10	2020-01-16
11	2020-01-23
12	2020-01-30	sheet08.pdf	sheet08-solution.pdf
13	2020-02-06	sheet09.pdf	sheet09-solution.pdf

Exams

• Main exam: Monday, February 10th, 2020, 10:00-12:00, at Geschwister-Scholl-Platz 01, room E 004
• Second exam: Thursday, April 2nd, 2020, 10:00-12:00, at Geschwister-Scholl-Platz 01, room M 218
• Second exam: Thursday, September 24, 2020, 10:00-12:00, at Oettingenstrasse 67, room B001

Literature

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.