News
- 2018.02.01: The last exerecise will be on Tuesday, 06.02.2018, at 12pm, in Oettingenstr. 67, room U151 (date and location of the lecture).
There will be no exercise on Thursday.
- 2018.01.19: The exam will be on Tuesday, 20.02.2018, at 12pm, in room A 125, Main Building.
- 2017.10.16: The first exercise will be next week, the 26.10. The lecture will start this week (i.e., tomorrow, the 17.10.)!
Topics
This lecture covers advanced topics of formal specification and verification.
It builds on the topics covered in the lecture "Formale Spezifikation und Verifikation 1" of the BSc-course.
- Data-flow Analysis, Software Model Checking
- Abstract Domains
- Interprocedural Analysis
- Predicate Analysis
- Satsfiability Modulo Theory (SMT)
- Interpolation
- Counterexample-Guided Abstraction Refinement
- Type Systems
- Automaton Models
- Verification Technology
Dates
- Lecture: Tue, 12 – 15 h, Oettingenstr. 67, Room U151 (17.10.2017 – 06.02.2018)
- Exercise: Thu, 12 – 14 h, Oettingenstr. 67, Room 161 (19.10.2017 – 08.02.2018)
There is no lecture on 31.10.2017 (holiday).
Detailed Time Table
| Date |
Lecturer |
Planned Topics |
| 17.10. |
DB + MH |
Organization, Introduction to lecture + lattices |
| 24.10. |
DB |
Dataflow analysis: Control-flow automata (CFAs)
+ Configurable program analyses (CPAs) |
| 31.10. |
- |
No lecture |
| 07.11. |
DB |
Abstract domains (reaching definitions, intervals, values) |
| 14.11. |
DB |
Counterexample-guided abstraction refinement (CEGAR) + Lazy abstraction |
| 21.11. |
DB |
Interpolation, Invariant synthesis |
| 28.11. |
DB |
Impact, predicate abstraction, k-induction, bounded model checking |
| 05.12. |
MH |
Interprocedural analysis |
| 12.12. |
MH |
Type systems |
| 19.12. |
MH |
Satisfiability modulo theories (SMT) |
| 09.01. |
MH |
IC3: Symbolic model-checking with BDDs, IC3 algorithm,
proofs of correctness and completeness |
| 16.01. |
MH |
Timed automata |
| 23.01. |
DB |
Technology: Witnesses, Visualization, Tools for Software Verification |
| 30.01. |
MH |
Hybrid automata (generalization of timed automata: arbitrary continuous variables) |
| 06.02. |
MH |
Generalizing counterexamples: certification of temporal properties
with parity games |
DB: Prof. Dr. Dirk Beyer
MH: Prof. Martin Hofmann, PhD
People
Learning Material
Copyright applies to the following learning material. Attendees of the lecture are permitted to use the material for their personal studies.
All other rights are reserved.
- Material of Prof. Beyer:
- Material of Prof. Hofmann:
Target Audience
MSc Computer Science (Informatik).
Participants may take part in the
joint training course (Praktikum)
offered.
Requirements
- Formale Spezifikation und Verifikation 1
Training (Praktikum)
A
joint training course (Praktikum) is available.
The training starts in the middle of the semester.
Literatur
Useful Links