On June 4, 1996 an unmanned Ariane 5 rocket launched by the ESA exploded just forty seconds after its lift-off from Kourou, French Guiana. The destroyed rocket was valued at $500 million. The cause of the failure was an uncatched exception caused by an unexpected conversion from a 64 bit floating point number to a 16 bit signed integer. Among 'victims' of other spectacular software bugs are Mars landers, Airbus aircraft, Pentium microprocessor floating point division, or Open SSL cryptography library. Some of the bugs caused not only financial losses but also human victims, for instance accidents in Therac-25 radiation therapy machine, or inaccuracies in time calculations in Patriot missiles.

The lecture is about methods of verification of computer systems that may increase reliability of computer systems. We focus on formal methods, based on rigorous mathematical foundations, and to a large extent automatic: model-checking, static analysis, and correctness proving. Most of our attention will be devoted to model-checking, that has been proved succesfull mostly in hardware verification, but there have been also some success stories in software verification. The current on-going research effort aims at appplying this approach, possibly in combination with the other formal methods, to verification of a wide range of software systems.

Topics:

  • introduction to formal verification
  • temporal logics: LTL, CTL, CTL*
  • omega-automata, LTL model-checking
  • partial-order reductions
  • BDD, symbolic CTL model-checking
  • bounded LTL model checking by reduction to SAT
  • abstraction methods (CEGAR)
  • static program analysis
  • abstract interpretation
  • requirements specification and correctness proofs
  • timed automata (optional)
  • probabilistic model-checking (optional)

Slides:


Tools:


Literature:


Books on formal verification:
  • E.M. Clarke, O. Grumberg, D.A. Peled, Model Checking. MIT Press, 2002.
  • B. Berard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, P. Schnoebelen, P. McKenzie, Systems and Software Verification. Springer, 2001.
  • C. Baier, J.-P. Katoen, Principles of Model Checking. MIT Press, 2008.
  • F. Nielson, H.R. Nielson, C. Hankin, Principles of Program Analysis, Springer, 2005.
  • K. Apt, E.-R. Olderog, Verification of Sequential and Concurrent Programs. Springer, 1997.
LTL, omega-automata and SPIN:
Symbolic model-checking and SMV:
Bounded model-checking:
Abstraction:
JML:
Timed automata:
  • R. Alur, D. L. Dill, A Theory of Timed Automata. Theoretical Computer Science 125:183-235, 1994.
  • R. Alur, Timed Automata. Proc. CAV'99, LNCS 1633, 8-22, Springer, 1999.
  • J. Bengtsson, W. Yi, Timed Automata: Semantics, Algorithms and Tools. Lecture Notes on Concurrency and Petri Nets, LNCS 3098, Springer-Verlag, 2004.
Probabilistic verification:
Model-checking success stories: