CIS 673: Computer-Aided Verification, Fall 2014
Class: Mon Wed 10.30-Noon, Towne 305
Introduction
How can a designer check that the system (s)he has designed works
correctly? Can an airline control system fail in a critical way when
a piece of hardware fails? Will a cache coherence protocol continue
to work correctly when an extra processor is added? Traditionally, designers
attempt to answer such questions using simulation over selected
sample cases. As computer systems become more complex and pervasive,
simulation-based techniques are not sufficient to assure desired
reliability. Model checking and related computer-aided verification
techniques are emerging as practical alternatives to simulation
for debugging complex systems. These methods allow the designer
to verify that a mathematical model of a system satisfies its
abstract logical specification.
This course is focused on training students in the basic principles of model checking.
Prerequisites
The course requires basic knowledge of algorithms, data structures,
programming languages, automata theory, computational complexity, and
propositional logic.
The course requires mathematical maturity, and is appropriate
for graduate students who wish to pursue research in
formal methods, software analysis, or related areas.
If you need more information to decide, contact the instructor.
Overview
Each week will focus on a selected chapter from Handbook of Model Checking, Springer, 2014.
The chapters of this upcoming Handbook are listed below. We can cover only a subset of these,
and the selection will be based on the interests of students.
The selected chapters will be distributed as reading material in advance.
- Chapter 1: What is Model Checking; Clarke, Henzinger, and Veith.
- Chapter 2: Temporal Logic; Piterman.
- Chapter 3: System Modeling; Seshia, Sharygina, and Tripakis.
- Chapter 4: Binary Decision Diagrams: An Algorithmic Basis for Symbolic Model Checking; Bryant.
- Chapter 5: Propositional SAT Solving; Malik and Marques-Silva.
- Chapter 6: Satisfiability Modulo Theories; Barrett and Tinelli.
Lectures by Leonardo De Moura: 1, 2, 3
- Chapter 7: Automata Theory and Model Checking; Kupferman.
- Chapter 8: The mu-calculus and Logical Foundations; Bradfield and Walukiewicz.
- Chapter 9: BDD-Based Symbolic Model Checking; Chaki and Gurfinkel.
- Chapter 10: SAT-based Model Checking; Biere and Kroening.
- Chapter 11A: Explicit State Model Checking; Holzmann.
- Chapter 11B: Partial Order Reduction; Peled.
- Chapter 12: Abstraction and Abstraction-Refinement; Dams and Grumberg.
Tutorial on BLAST software model checker
- Chapter 13: Compositional Reasoning; Giannakopoulou, Namjoshi, and Pasareanu.
Tutorial by Giannakopoulou and Pasareanu
- Chapter 14A: Interpolation: Proofs in the Service of Model Checking; McMillan.
- Chapter 14B: Combining Model Checking and Theorem Proving; Shankar.
- Chapter 15A: Transferring Model Checking Technology to Industry; Kurshan
- Chapter 15B: Hardware Specification Languages; Eisner and Fisman.
- Chapter 16: Software Verification by Predicate Abstraction; Jhala, Podelski, and Rybalchenko.
- Chapter 17: Model Checking Concurrent Software; Gupta, Kahlon, Qadeer, and Touili.
Lectures by Arjun Radhakrishna:
Part 1; Part 2
- Chapter 18: Combining Model Checking and Data-Flow Analysis; Beyer, Gulwani, and Schmidt.
- Chapter 19: Combining Model checking and Program Testing; Godefroid and Sen.
Slides by Sen on CUTE,Slides by Godefroid on SAGE
- Chapter 20: Symbolic Trajectory Evaluation; Melham,
- Chapter 21: Model Checking Procedural Programs; Alur, Bouajjani, and Esparza.
Slides from Marktoberdorf Summer School
- Chapter 22: Parametrized Verification; Abdulla, Sistla, and Talupur.
- Chapter 23: Model Checking and Process Algebra; Cleaveland, Roscoe, and Smolka.
- Chapter 24: Model Checking Security Protocols; Basin, Cremers, and Meadows.
- Chapter 25: Graph Games and Reactive Synthesis; Bloem, Chatterjee, and Jobstmann.
- Chapter 26: Symbolic Model Checking in Non-Boolean Domains; Majumdar and Raskin.
- Chapter 27: Verification of Real-Time Systems; Bouyer, Fahrenberg, Larsen, Markey, Ouaknine, and Worrell.
- Chapter 28: Verification of Hybrid Systems; Doyen, Frehse, Pappas, and Platzer.
- Chapter 29: Probabilistic Model Checking; Baier, de Alfaro, Forejt, and Kwiatkowska.
Tutorial by Marta Kwiatkowska: Part 1, Part 2
- Syntax-Guided Synthesis
Logistics
Every week, students are expected to read the chosen chapter, before
the lectures, and participate actively during class.
Each student is also expected to do a project and give a presentation at the end of the semester.
There will be no homeworks or exams.
Maintained by Rajeev Alur