Aktuelles
- 2018.02.01: Die letzte Übung ist am Dienstag, 06.02.2018, um 12.00, in Oettingenstr. 67, Raum U151 (Ort und Zeit der Vorlesung).
Die Übung am folgenden Donnerstag entfällt dafür.
- 2018.01.19: Die Klausur findet statt am Dienstag, 20.02.2018, um 12 Uhr, in Raum A 125, Hauptgebäude.
- 2017.10.16: Die erste Übung findet nächste Woche, den 26.10, statt. Die Vorlesung beginnt diese Woche (d.h. morgen, den 17.10.)!
Inhalt
Diese Vorlesung ist eine Fortführung und Vertiefung der Veranstaltung
Formale Spezifikation und Verifikation im BSc-Studium.
- Datenflussanalyse, Software-Model-Checking
- Abstract Domains
- Interprocedural analysis
- Praedikatenanalyse
- Satsfiability Modulo Theory (SMT)
- Interpolation
- Counterexamples
- Counterexample-Guided Abstraction Refinement
- Typensysteme
- Automatenmodelle
- Verifikations-Technologien
Termine
- Vorlesung: Di, 12 – 15 Uhr, Oettingenstr. 67, Raum U151 (17.10.2017 – 06.02.2018)
- Übung: Do, 12 – 14 Uhr, Oettingenstr. 67, Raum 161 (19.10.2017 – 08.02.2018)
Am 31.10.2017 findet keine Vorlesung statt (Feiertag).
Zeitplan
| Datum |
Dozent |
Geplante Themen |
| 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
Personen
Materialien
Die folgenden Materialien unterliegen dem Copyright. Teilnehmern der Vorlesung ist die Verwendung für persönliche Studien gestattet. Alle anderen Rechte sind vorbehalten.
- Material von Prof. Beyer:
- Material von Prof. Hofmann:
Hörerkreis
Master Informatik, gleichzeitiger Besuch des
Praktikums zur Veranstaltung möglich.
Benötigte Vorkenntnisse
- Formale Spezifikation und Verifikation 1
Praktikum
Es wird ein
vorlesungsbegleitendes Praktikum angeboten.
Beginn des Praktikums ist zur Mitte des Semesters.
Literatur
Nützliche Links