To the English version

Formale Spezifikation und Verifikation 2

Aktuelles

Inhalt

Diese Vorlesung ist eine Fortführung und Vertiefung der Veranstaltung Formale Spezifikation und Verifikation im BSc-Studium.

Termine

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.

Hörerkreis

Master Informatik, gleichzeitiger Besuch des Praktikums zur Veranstaltung möglich.

Benötigte Vorkenntnisse

Praktikum

Es wird ein vorlesungsbegleitendes Praktikum angeboten.
Beginn des Praktikums ist zur Mitte des Semesters.

Literatur

Nützliche Links