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:
- Slides 0: an ad
- Slides 1: Overview of formal methods
- Slides 2: LTL
- Slides 3: LTL and omega-automata
- Slides 4: LTL model cheking
- Slides 5: CTL
- Slides 6: Symbolic verification
- Slides 7: Bounded verification
(continuation on software verification)
- Slides 8: Abstraction-based verification
- Slides 9: Abstract interpretation
- Slides 10: Model-checking success stories
Tools:
Literature:
- 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.
- G. J. Holzmann, The SPIN Model Checker. Pearson Educational, 2003.
- M. Ben-Ari, Principles of the SPIN Model Checker. Springer, 2008.
- G.J. Holzmann, D.A. Peled, An Improvement in Formal Verification. Proc. FORTE 1994.
- G.J. Holzmann, D.A. Peled, M. Yannakakis, On nested depth-first search. Proc. of the 2nd Spin Workshop, pp. 23-32, 1996.
- P. Gastin, D. Oddoux, Fast LTL to Büchi Automata Translation. Proc. CAV'01, LNCS 2102, p. 53-65.
- S. Demri, Ph. Schnoebelen, The Complexity of Propositional Linear Temporal Logics in Simple Cases. Information and Computation 174(1), str. 84-103, 2002.
- E. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith, Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752-794, 2003.
- E. Clarke, O. Grumberg, D. Long, Verification tools for finite-state concurrent systems. In: A Decade of concurrency--Reflections and Perspectives, LNCS 803, 1994.
- K.L.McMillan, Symbolic Model Checking. praca doktorska, 1992.
- R. E. Bryant, Symbolic boolean manipulation with ordered binary decision diagrams. ACM Computing Surveys 24(3):293-318, 1992.
- A. Biere, A. Cimatti, E.M. Clarke, O. Strichman, Y. Zhu, Bounded Model Checking. Advances in Computers 58, 2003.
- E. M. Clarke, A. Biere, R. Raimi, Y. Zhu, Bounded Model Checking Using Satisfiability Solving. Formal Methods in System Design 19(1): 7-34, 2001.
- D. Kroening, E. M. Clarke, F. Lerda, A Tool for Checking ANSI-C Programs. Proc. TACAS 2004, 2004.
- D. Kroening, E. M. Clarke, K. Yorav, Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking. Proc. DAC 2003, 2003.
- E. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith, Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752-794, 2003.
- T. Ball, S. K. Rajamani, Boolean Programs: A Model and Process for Software Analysis, technical report, Microsoft research, 2000.
- E. Clarke, D. Kroening, N. Sharygina, K. Yorav, Predicate Abstraction of ANSI-C Programs using SAT, Formal Methods in System Design 25, 105-127, 2004.
- P. Cousot, R. Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. Proc. POPL'77, str. 238—252, 1977.
- N. D. Jones, F. Nielson, Abstract Interpretation: a Semantics-Based Tool for Program Analysis. Handbook of Logic in Computer Science, tom 4, str. 527-636, 1995.
- Abstract Interpretation, strona WWW utrzymywana przez P. Cousot.
- V. D'Silva, D. Kroening, G. Weissenbacher, A Survey of Automated Techniques for Formal Software Verification. IEEE Trans. on CAD of Integrated Circuits and Systems 27(7):1165-1178, 2008.
- G. T. Leavens, Y. Cheon, Design by Contract with JML.
- P. Chalin, J. R. Kiniry, G. T. Leavens, E. Poll, Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2. FMCO 2005, 342-363.
- J. R. Kiniry, G. T. Leavens, E. Poll, A JML Tutorial: Modular Specification and Verification of Functional Behavior for Java. CAV 2007 Tutorial
- K. Rustan, M. Leino, G. Nelson, J.B. Saxe, ESC/Java User’s Manual.
- 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.
- M. Kwiatkowska, Model checking for probability and time: from theory to practice. Proc. LICS'03, pp. 351-360, 2003.
- D. Parker, Implementation of Symbolic Model Checking for Probabilistic Systems. Praca doktorska, Uniwersytet w Birmingham, 2002.
- A. Miner and D. Parker, Symbolic Representations and Analysis of Large Probabilistic Systems. Proc. Validation of Stochastic Systems: A Guide to Current Research, LNCS 2925, 2004.
- M. Fujita, P.C. McGeer, J.C.-Y. Yang, Multi-Terminal Binary Decision Diagrams: An Efficient Data Structure for Matrix Representation. Formal Methods in System Design 10:149-169, 1997.
- G. J. Holzman, Mars Code. Commun. ACM 57(2):64-73, 2014.
- D.L. Detlefs, C.H. Flood, A.T. Garthwaite et al. Even better DCAS-based concurrent deques. Distributed Algorithms, LNCS Vol. 1914, 59–73, 2000.
- S. Doherty et al. DCAS is not a silver bullet for nonblocking algorithm design. SPAA 2004: 216-224, 2004.
- T. Ball, V. Levin, S. K. Rajamani, A decade of software model checking with SLAM. Commun. ACM 54(7):68-76, 2011.
- T. Ball, S. K. Rajamani, Bebop: a symbolic model-checker for boolean programs. SPIN Workshop, LNCS 1885, pp 113-130, 2000.