Announcements
- Final marks and grades are here.
- The end-term exam is on April 23, 2011 from 9am-12pm in lecture hall (117).
- The class on April 21, 2011 will be held in multimedia classroom (252).
- Updated marks after the 2nd midterm are here.
- The schedule of seminars is announced.
- Seminar topics are annouced. Written submission of seminar example is due on March 24, 2011 in the class.
- Homework 2 is due on March 8, 2011 in the class.
- Marks of Midterm 1 are here.
- Marks of Homework 1 are here.
- Homework 1 is due on Feb 3, 2011 in the class.
- Organizational class: On January 6th at 3.30pm
Introduction
Computer systems in today's world are large, complex, costly, and perhaps safety-critical.
Their correctness is as critical as their performance.
While testing is an indispensable technique for exploring behaviors of systems,
it can rarely cover all behaviors of the system. Many bugs still make it past testing.
Automated verification is an alternative to testing wherein a mathematical model of
a system is built and analyzed, algorithmically, with respect to logical specifications.
Some examples of successful applications of verification to real world systems are
IEEE Futurebus+ cache coherence protocol, primary flight control software of Airbus A340, and Windows device drivers.
In this course, we will discuss formal modeling of systems and logical specifications of their properties.
Our focus will be on understanding the core algorithmic techniques for formal analysis.
Course contents
- Formal models of systems: simple programs, state transition diagrams, Kripke structures
- Specification logics: propositional and first-order logic; temporal logics (CTL, LTL, CTL*); fixpoint logic: mu-calculus
- Algorithmic analysis: satisfiability checking; decision procedures for satisfiability modulo theories; model checking: explicit, automata-theoretic, and symbolic
Course evaluation
- Homeworks: Two homework assignments of problem solving nature will be given.
- Mid-term exams: Two topic-wise mid-term exams will be conducted.
- Seminar: Every student will be assigned a topic for presentation.
- End-term exam: An end-term exam covering the entire course contents will be taken.
Reference texts
- Michael Huth, Mark Ryan: Logic in Computer Science: Modelling and Reasoning about Systems, Cambridge University Press, 2004.
- Daniel Kroening, Ofer Strichman: Decision Procedures: An Algorithmic Point of View, Springer, 2008. Also available online.
- Edmund M. Clarke, Orna Grumberg, Doron Peled: Model Checking, MIT Press, 2001.
- Christel Baier, Joost-Pieter Katoen: Principles of Model Checking, MIT Press, 2008.
Slides and other material
The slides on propositional and first-order logic are adapted from slides available
here.
- Propositional logic primer (Lectures 2,3): slides
- SAT solvers (Lectures 4,5): slides
- Binary decision diagrams (Lecture 6): slides, notes
- First order theories (Lecture 7): slides
- Equality logic with uninterpreted functions (Lectures 8,9): slides
- Equality logic decision procedures (Lectures 10,12): slides slides
- Linear arithmetic: Simplex (Lectures 13,14): slides, notes
- Integer linear arithmetic: Branch and bound slides,
Fourier-Motzkin variable elimination (Lecture 15) slides
The slides on temporal logic are adapted from slides available
here.