ws18 fmsoft

Depending on schedules of participants, there is small chance of adjustments if necessary.

Some slides are going to be protected by a password the participants of the course will obtain directly from me.

• The opening slides with sales talk
• General introduction to model checking and temporal logic (16 Oct)pre-lecture version
• Introducing LTL (23 Oct)pre-lecture version
• Introducing CTL (30 Oct, pre-lecture version)
• Introducing CTL (6 Nov, lecture version)pre-lecture version
• Model checking for CTL (13 Nov, lecture version) pre-lecture version
• Unifying CTL and LTL: CTL^* (20 Nov, lecture version)pre-lecture version
• Bounded model checking (27 Nov, lecture version)pre-lecture version
• Beginning Hoare logic (4 Dec, lecture version)
• Frame your reasoning (11 Dec, lecture version)pre-lecture version
• Beginning denotational semantics (18 Dec, handout version)
• Kleene Theorem and denotational semantics of loops (Jan 8)
• Weakest liberal preconditions and relative completeness (Jan 15)
• Expressivity, total correctness, decorated programs (Jan 22)
• Weakest preconditions in separation logic (Jan 29)pre-lecture version
• Annotated programs and verification conditions in separation logic (Feb 5, handout version)

Tutorial page for FMSoft

See here.

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 frama-c
• 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.

• G. Winskel: The Formal Semantics of Programming Languages: An Introduction, The MIT Press, 1993.
• Ch. Baier, J-P. Katoen, Principles of Model Checking, The MIT Press, 2008.
• M. Huth, M. Ryan: Logic in Computer Science, Cambridge University Press, 2. Aufl., 2004.