Software Model Checking

— Course Description —

Synopsis




Lecture topics



  1. Automated software analysis: what and why?
  2. Overview of reliability methods: program testing; static analysis; deductive techniques; model checking
  3. Examples of model checkers: what can, and can't, they do
  4. Model checking: first principles
  5. Temporal logic as a specification mechanism
  6. Temporal logic model checking
  7. Symbolic reasoning (i): transition graphs as propositional formulas; formulas as decision diagrams
  8. Abstraction: state explosion; existential vs. universal, soundness; (bi-)simulation; counterexample-guided refinement
  9. Symbolic reasoning (ii): SAT-based bounded model checking
  10. Symbolic reasoning (iii): programs as first-order formulas; SMT solving; bounded and unbounded model checking; completeness
[Note: This course is not about classic static analysis methods, such as control- or dataflow analyses, pointer analysis, etc: these methods directly analyze programs (source code), while in formal verification we analyze formal models of programs. We may use such methods as tools, but we will not study them.]

Relevant books



You do not need to buy any book for this class — we will gather all required material from papers and lectures. However, if you like learning from (or being accompanied by) a book, I recommend the first one below.
  1. Christel Baier and Joost-Pieter Katoen: Principles of Model Checking. MIT Press, 2008. ISBN 978-0-262-02649-9

    This is the most comprehensive and up-to-date book on the subject. It includes much of what we will cover in this class, plus more specialist topics such model checking with timing constraints, and probabilistic model checking.

  2. Michael Huth and Mark Dermot Ryan: Logic in computer science — Modelling and reasoning about systems (2nd ed.). Cambridge University Press, 2004. ISBN 978-0521543101

    This one is more light-weight and emphasizes logic (it offers a logic survey, predicate logic, SAT, and temporal logics) more than the practical aspects of program verification (it does not cover remedies to the state explosion problem, abstraction techniques, etc.).

  3. Edmund M. Clarke and Orna Grumberg and Doron Peled: Model checking. MIT Press, 2001. ISBN 978-0-262-03270-4

    This one is rather old by now. It does not cover the more modern topics of SAT/SMT-based model checking and predicate abstraction. It does present lots of classic material from the area.

How this class works: Overview



This class consists of:

Details on "Serious paper reading" assignments



These assignments cover parts of the foundational concepts of this class. Since I want everyone to walk out of this class understanding these concepts, we will go through them in class (rather than delegating their absorption entirely to self-guided reading), as follows: one student will introduce the material in a short tutorial-style lecture. Everyone else will submit a roughly one-page write-up on the topic; guidance on what to write will be given in each case.

The lectures are in part supposed to give you a chance for some light-weight presentation practice. "Light-weight" means the presentation is relatively short (conference length), and the topic will not be excessively deep. Nonetheless it will be new for you, so you must make an effort to get on top of the material. We will conclude with a brief evaluation of the presentation.

Action items for presenter:

Action items for everyone else:


Schedule for tutorial presentations

DATE TOPIC PRESENTER ASSIGNED READING OTHER RESOURCES; GUIDANCE
Wed, Jan 27 The SPIN Model Checker Leif Andersen Gerard Holzmann: The Model Checker SPIN. IEEE TOSE, 1997 Presenter: start at the main SPIN website. Discuss principal features, and give a demo.

Everyone: focus on the pragmatic aspects of the paper: expressiveness of input and specification language, feedback given, etc.
At this stage of the class you may mostly skip the algorithmic details (Section 3).
Wed, Jan 27 Formal Methods at POPL 2016 Max New POPL 2016 Presenter:
  • give an overview of formal reasoning topics at POPL 2016 (both research papers and tutorials)
  • pick one that you would like to say more about, and do that. (No full paper presentation required.)
Everyone: no one-page reading report required for this tutorial!
Nonetheless, look at the POPL 2016 page and see what is out there, so that we can have a meaningful discussion.
Wed, Feb 10 Stateless Search in Verisoft Sam Caldwell Patrice Godefroid: Model Checking for Programming Languages using Verisoft. POPL, 1997 Presenter:
  • Focus on the contrast to standard state-aware model checking (which we will have covered by then): advantages/disadvantages.
  • Where does stateless search stand today — is it used? is it forgotten? tools?
Thu, Feb 11 Proving Termination Konstantinos Athanasiou Byron Cook, Andreas Podelski, Andrey Rybalchenko: Termination Proofs for Systems Code. PLDI, 2006 Presenter:
  • We will likely not spend much time on termination either before or after your presentation, so do talk about foundations of the technique
  • Do some on-board examples; tool demos not required (but not forbidden)
Wed, Feb 17 Lazy Abstraction Kevin Clancy Tom Henzinger, Ranjit Jhala, Rupak Majumdar, Gregoire Sutre: Lazy Abstraction. POPL, 2002
Mon, Feb 22 Predicate Abstraction for the C Language Yijia Gu Thomas Ball, Rupak Majumdar, Todd D. Millstein, Sriram K. Rajamani: Automatic Predicate Abstraction of C Programs. PLDI, 2001
Mon, Feb 29 Craig Interpolation in Model Checking Ben Greenman Kenneth McMillan: Applications of Craig Interpolants in Model Checking. TACAS, 2005
Kenneth McMillan: Lazy Abstraction with Interpolants. CAV, 2006
Presenter:
  • define Craig interpolants, and give examples
  • briefly mention/sketch their many uses in verification
  • discuss their use in symbolically proving properties over paths with loops; see the CAV 2006 paper
Wed, Mar 02 Decision Procedures Overview Peizun Liu Daniel Kroening, Ofer Strichman: Decision Procedures – An Algorithmic Point of View. Springer-Verlag Berlin/Heidelberg, 2008
(You can get this book in the library.)
Presenter: you should cover:
  • what theories exist? (include software-relevant theories, such as arrays, bitvectors)
  • what are the basic complexity results; what is decidable?
  • what tool support exists?
Another good reference is the SMT Lib website (just a resource; do not focus on the SMT Lib)
Everyone: no one-page reading report required for this tutorial!
Wed, Mar 02 Separation Logic Benjamin Chung John C. Reynolds: Separation Logic: A Logic for Shared Mutable Data Structures. LICS, 2002 See also: An Overview of Separation Logic
Wed, Mar 16 Probabilistic Model Checking Andrew Cobb Vicky Hartonas-Garmhausen, Sergio Campos, Edmund Clarke: ProbVerus: Probabilistic Symbolic Model Checking. ARTS, 1999 This is very sketchy, but gives a breadth-first overview. We will likely look at timed temporal logics more in future sessions.
Mon+Wed, Mar 21+23 Timed and Hybrid Systems Overview Thomas Wahl Oded Maler, Zohar Manna, Amir Pnueli: From timed to hybrid systems. REX Workshop, 1991 A good overview/survey. More technicalities (but less breadth) in: Thomas A. Henzinger, Zohar Manna, Amir Pnueli: Temporal Proof Methodologies for Real-time Systems. POPL, 1991.
We will also look at timed automata this week (no reading assignment on that part).
Mon, Mar 28 Concurrency Thomas Wahl Sarita Adve, Hans-J. Boehm: Memory Models: A Case for Rethinking Parallel Languages and Hardware. CACM, 2010 We will discuss: (a) Foundational Results in (Reordering-Free) Concurrency; (b) Memory Models in Software and Hardware.
No reading is required for (a). The assigned reading gives a good and relatively light overview on (b).


Details on topic explorations



Topic exploration allows you to work on something that you pick (with gentle guidance by me). This could be some aspect that just plainly interests you, or it could be something coming out of your own research where you feel the use of formal verification and model checking can be of use. Or it could be something else. Here are some sample categories: Topics need to be approved by me; in due time I will ask you for a brief write-up (a few paragraphs) of a topic proposal. Given the expected small size of the class, I do not anticipate group projects, unless the topic you pick strongly suggests it.

Topic explorations conclude with:
Submission deadline for written reports: Thu Apr 28, 11:59pm

Presentation schedule

DATE TITLE PRESENTER ARTWORK
Wed, Mar 30Verifying an Optimization Phase of the Nanopass Compiler Leif Andersen Nanopass
Wed, Mar 30KodKod^2: Porting Kodkod from Java to Racket Ben Greenman Cake
Mon, Apr 04Abstract Interpretation for Tracking Numerical Error Kevin Clancy Numerical Error
Mon, Apr 04Dynamic Analysis of the Stability of Floating-Point Programs Yijia Gu instable
Wed, Apr 06On Masking Countermeasures against FP-based Timing Attacks Konstantinos Athanasioumasking
Mon, Apr 11Towards Optimizing Broadcast Preimage Computation Peizun Liu broadcast
Wed, Apr 13A model checker for Network Calculus Sam Caldwell
Wed, Apr 25Gradual Typing as Abstract Interpretation Max New
Mon, Apr 25Formal Verification of C components of dynamic programming languagesBen Chung


Grading



There will be various course component grades, which contribute to your course grade as follows: There will be no exams.

Academic Integrity and Professionalism



Standard University rules apply. Cooperation is generally encouraged, but you must always give proper credit to your collaborators. In some cases, your individual contribution will need to be measured, as for the case of homeworks.
We also apply standard rules of promptness of homework and report submissions. If you feel you will be late, bring this up in time, so we can see whether to extend (for everyone) any deadline. Individual exceptions are unfair and will generally not be granted.