Software Model Checking

— Course Description —

Synopsis

Course number: CS 7485
Class times: Mon & Wed, 2:50pm–4:30pm
Class location: Ryder Hall 435
Instructor: Thomas Wahl
Office hours: after each class meeting or by appointment, room 344, West Village H (my office)

Lecture topics

Automated software analysis: what and why?
Overview of reliability methods: program testing; static analysis; deductive techniques; model checking
Examples of model checkers: what can, and can't, they do
Model checking: first principles
Temporal logic as a specification mechanism
Temporal logic model checking
Symbolic reasoning (i): transition graphs as propositional formulas; formulas as decision diagrams
Abstraction: state explosion; existential vs. universal, soundness; (bi-)simulation; counterexample-guided refinement
Symbolic reasoning (ii): SAT-based bounded model checking
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.

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.

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.).

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:

Lectures: they cover the material listed under Lecture topics. These lectures will mostly be given by the instructor and will happen during the first half of the course.

Homework exercises: there will be a few, mostly accompanying the lectures. They are for you to test your understanding of the material, so you are encouraged to work on these exercises alone.

Light paper reading: for background information, historical perspective, classics, etc. These readings accompany the lectures and are mostly offered for your intellectual entertainment. We may briefly discuss them in the subsequent lecture, especially if you have comments or questions.

Serious paper reading: some lecture topics are directly taken from papers. For each such topic, one student will be selected to cover it by way of a tutorial presentation. (These presentations are interleaved with the initial lectures by the instructor.) Details about this are given below.

Topic exploration: each student will work on a topic of their choice (related to the course agenda) in greater depth. This work can take many forms; possible categories are listed below. This will happen mostly in the second part of the course. At the end of the class, everyone will give a full-length presentation of the results of this topic exploration, and submit a short-paper style written report.

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:

prepare an approximately 30min presentation (the whole "session" with Q&A is supposed to last about 45min = 1/2 class).

Make your presentation engaging, use examples, and ask questions.

turn in your "presentation plan" to me 3–5 days before your scheduled day. Your plan may contain slides, or otherwise an outline of the organization if you are not using slides.

Action items for everyone else:

study the assigned paper(s) (occasionally this may also include tools or websites)

write a one-page reading report. The format is relatively free and depends on the flavor of the subject. Unless otherwise stated, the report should:
- summarize the contents (for research papers this should include at least an attempt to critique the results, including what you liked/didn't like about them)
- formulate 1–2 questions that we can discuss in class (time permitting; not all written questions will be discussed).

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:

the study of a new theme/aspect of formal verification not covered in the lectures;
a practical verification effort, consisting of using an existing model checker to analyze a non-trivial piece of software;
solving a particular technical/theoretical problem related to verification;
the implementation and evaluation of some (ideally recent) model checking algorithm;
a comparative study of different techniques that address similar problems.

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:

a presentation of the results at the end of the class. The presentation should be about 45—60min in length. We will discuss the format of these presentations in class. As a rule of thumb, in contrast to the tutorials, these presentations will be longer and more in depth.
a short-paper style written report. This should in most cases be a (short) research essay, i.e. it must clearly state what topic you are exploring, why this is interesting, what else is out there on this topic, why that is insufficient, what you have done, and what results/insights you have obtained. Depending on the type of topic you are exploring, these guidelines may deviate. For instance, in the case of a study of a textbook theme not covered in the lectures, no previously unknown results/insights are expected.
It is fine for topic explorations to end "partially inconclusive": if you find that some aspects are unclear and require further work, state so in your report.

Submission deadline for written reports: Thu Apr 28, 11:59pm

Presentation schedule

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

Grading

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

Homework exercises: 10%
Light paper reading: 0%
Serious paper reading: written summary: 10%
Serious paper reading: tutorial: 20%
Topic exploration: report: 20%
Topic exploration: presentation: 30%
Class participation: 10%

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.