ws16 fmsoft
Formale Methoden der Softwareentwicklung
Dozenten  Dr Tadeusz Litak und Christoph Rauch 
Umfang  Vorlesung+Übung, 4 SWS, ECTSCredits: 7,5 
Achtung: Die Vorlesung am Mittwoch, 16:15–17:45 findet im Raum 00.131128 01.255128 02.133113 statt.
See also the UnivIS entry.
Tutorials
Please see dedicated webpage for these.
Ziel: Werkzeuge für die Korrektheit von Programmen und Systemen

Theorie und Praxis automatischer Verfahren zur Korrektheitsprüfung

Umgang mit aktuellen Werkzeugen für fehlerfreien Code
Inhalt
In the first part of the course, we will engage in the formal verification of reactive systems. Students learn the syntax and semantics of the temporal logics LTL, CTL, and CTL* and their application in the specification of e.g. safety and liveness properties of systems. Simple models of systems are designed and verified using model checkers and dedicated frameworks for asynchronous and synchronous reactive systems, and the algorithms working in the background are explained.
The second part of the course focuses on functional correctness of programs; more precisely, we discuss the theory of pre and postconditions, Hoare triples, loop invariants, and weakest (liberal) preconditions, in order to introduce automatised correctness proofs using the Hoare calculus.

Tools we are planning to use for the first part of the material include at least the model checker nuSMV/nuXmv.

Tools we are planning to use for the second part of the material include at least the framework framac

Depending on whether there is more interest in the first or in the second part (and on other factors), we will devote the remaining tutorials either to SCADE or to VeriFast, correspondingly.
Lecture notes
That is, all the slides below zipped and, importantly, converted to a handout format (none of these pesky overlays, suitable for printing). Protected with the same password as slides.
Slides

Slides of the first lecture (protected): a general introduction to Formal Methods

Slides of the second lecture (protected): introduction to model checking and temporal logic

Slides of the third lecture (protected): LTL and CTL

Slides of the fourth lecture (protected): recursive equations and fixpoints

Slides of the fifth lecture (protected): fixpoints and model checking

Slides of the sixth lecture (protected): model checking and fairness

Slides of the seventh lecture (protected): introduction to semantics of programs

Slides of the eighth lecture (protected): domains, fixpoints and denotational semantics

Slides of the ninth lecture (protected): soundness of Hoare rules

Slides of the tenth lecture (protected): weakest preconditions and relative completeness

Slides of the eleventh lecture (protected): frame your reasoning—introduction to shared mutable data structures

Slides of the twelfth lecture (protected): dynamic IMP and its Hoare logic

Slides of the thirteenth lecture (protected): Separation Logic—w(l)p and vcfriendly specifications

Slides of the fourteenth lecture (protected): annotated programs and total correctness

Slides of the fifteenth lecture (protected): bounded model checking
Literatur

G. Winskel: The Formal Semantics of Programming Languages: An Introduction, The MIT Press, 1993.

M. Huth, M. Ryan: Logic in Computer Science, Cambridge University Press, 2. Aufl., 2004.