CPSC 513 Winter 2008-2009 Term 1 Class Home Page

Integrated Systems Design:

Introduction to Formal Verification

Contents of this page


Growing Set: avi mpg
Final Set: avi mpg

Late Breaking News:

Handouts

Hard copies are not distributed in class -- if you want one, print it.

# Date Topic
1 Monday, October 6 Guidelines for Reading & Reviewing Papers
2 Tuesday, October 28 Course Project Overview
3 Thursday, November 20 Course Project Presentations
3 Monday, December 1 Course Project Final Reports

Homeworks

Homework Submission Policy:

# Due Date Assignment Assignment Links Solution Solution Links
1 October 2 Problem Set Question 4: BDD version or SAT version. None. None.
2 October 21 Problem Set Links for the Murphi components. None. None.
3 November 13 Problem Set None. None. None.
4 November 28 Problem Set None. None. None.

Course Overview

What this course is not: The official title "Integrated Systems Design" of CPSC 513 is an historical misnomer. The course is actually about formal verification of systems constructed from computer hardware, software or some combination of both. The course content has been redirected for two reasons. First, more professors in the department are working in verification than in design. Second, demand from industry for graduates skilled in verification techniques is outstanding.

What this course is: An introduction to formal verification, so that students can get an overview of the field. Evaluation will be a combination of homeworks, paper presentations and a course project. The course should be approachable and applicable to students throughout computer science. Students interested in pursing further study and research of formal verification will be equipped to work with and/or take advanced courses from the ISD professors (Mark Greenstreet, Alan Hu and Ian Mitchell).

This course shares a fair amount of content with the most recent previous CPSC 513 offerings: 2007 (taught by Alan Hu) and 2005 (taught by Ian Mitchell).

Motivation: A central feature of modern design methods is the modeling and simulation of the system as early and as often as possible, since models and simulations are usually much cheaper, faster and safer to construct than physical prototypes. However, for many complex systems the costs and challenges of exhaustive simulation have become overwhelming.

The field of formal verification uses mathematical reasoning about system models to draw conclusions about system behavior without exhaustive simulation. It has been applied to systems including:

  • The analog propagation of charge through wires and transistors of integrated circuits.
  • The digital operation of arithmetic/logic units and register files in computer chips.
  • Communication protocols for caches and computer networks.
  • Integrated hardware/software embedded systems in consumer electronics.
  • Collision avoidance procedures for vehicles such as cars and aircraft.
  • Small but critical software services such as operating system device drivers.

While of particular interest in safety critical systems -- such as the computers which maintain the stable flight of modern aircraft -- formal methods have also found fertile ground in applications where they can more quickly and/or cheaply provide test coverage than simulation based approaches.

Topics (in brief):With so many different application areas, it is not surprising that this field draws on many sub-disciplines of computer science, engineering and mathematics. In the limited time available, this course will touch only on a subset of the formal verification field, including:

  • Models of computation for concurrent, real-time, continuous and hybrid systems.
  • Formal methods of specification, abstraction and refinement.
  • Conceptual tools such as invariants, reachability, fixpoint iteration, weakest precondition and assume/guarantee.
  • Algorithms and implementations such as binary decision diagrams (BDDs), satisfiability, symbolic model checking, automated theorem proving and Lyapunov functions.

Expectations: In addition to attending lectures, students will:

  • Read and discuss academic papers.
  • Complete several homework assignments involving both paper and pencil and programming components.
  • Complete a project involving some aspect of formal verification. The project will include a proposal, a presentation and a brief written report.


Course Details

Intended Audience: Graduate students in

Prerequisites: Graduate standing or consent of the instructor.

Grades: Your final grade will be based on a combination of:

The relative weighting will depend on how many homework assignments I come up with.

Instructor: Ian Mitchell

Lectures: 14:00 - 15:30, Tuesdays and Thursdays, ICCS 238.

References: There is no textbook for the course. Readings will come from original research papers listed (and linked) in the Schedule below. Background and additional material can be found in the Links below, or in the following books:

The Schedule:

# Date Topic Links Required Readings Optional Readings
Sept 2 & 4 Graduate Student Orientation. No Lectures.
1 Sept 9 Introduction. A taste of Hybrid System Reachable Sets. Introduction slides (including syllabus handout). 2007 ACM Turing Award Press Release. None. Leah Hoffman, "In Search of Dependable Design" in Communications of the ACM, vol. 51, num. 7, pp. 14-16 (July 2008). Leah Hoffman, "Q&A: Talking Model Checking Technology" in Communications of the ACM, vol. 51, num. 7, pp. 110-112 (July 2008).
2 Sept 11 Circuits and Boolean Formulae. Canonical forms and Equivalence Checking. Logic gate truth tables from Wikipedia, the University of Maryland or the Electronics Club at Kelsey Park School. Edmund M. Clarke & Robert P. Kurshan, "Computer-Aided Verification" in IEEE Spectrum, June 1996, pp. 61-67 None.
3 Sept 16 Ordered Binary Decision Diagrams. None. Randal E. Bryant, "Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams" in ACM Computing Surveys, Vol. 24, No. 3 (September 1992), pp. 293-318. Henrik Reif Andersen, "An Introduction to Binary Decision Diagrams".
4 Sept 18 BDD Canonicity. BDD operations. BDD implementation and Complexity. Guest Lecturer Mark Greenstreet. CU Decision Diagram Package (CUDD), a package for manipulation of BDDs and other species of decision diagrams. Karl S. Brace, Richard L. Rudell & Randal E. Bryant, "Efficient Implementation of a BDD Package" in 27th Design Automation Conference, pp. 40-45 (1990). Randal E. Bryant, "On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Applications to Integer Multiplication" in IEEE Transactions on Computers, Vol. 40, No. 2, pp.205-213 (February 1991).
5 Sept 23 An Analog Verification Digression. Guest Lecturer Mark Greenstreet. None. Mark R. Greenstreet & Suwen Yang, "Verifying start-up conditions for a ring oscillator" in Proceedings of the 18th ACM Great Lakes Symposium on VLSI, pp. 201-206 (May 2008). None.
6 Sept 25 SAT Solvers and Verification. Guest Lecturer Alan J. Hu. MiniSat, a "minimalistic open-source SAT solver". Lintao Zhang and Sharad Malik, "The Quest for Efficient Boolean Satisfiability Solvers" in Proceedings of 14th Conference on Computer Aided Verification (CAV 2002 in Copenhagen, Denmark), LNCS 2404, pp. 17-36 (July 2002). Alan's additional explanation of implication graphs and learning, based in part on Lintao Zhang, Conor F. Madigan, Matthew H. Moskewicz, Sharad Malik, "Efficient Conflict Driven Learning in a Boolean Satisfiability Solver" in ICCAD 2001, pp. 279-285. An even broader survey is Vipin Kumar, "Algorithms for Constraint Satisfaction Problems: A Survey" in AI Magazine, volume 13, number 1, pp. 32-44, (1992).
7 Sept 30 Equivalence Checking Wrap-up. Introduction to Systems with State. Markov Assumption. Wikipedia entries for State transition system and Markov process. Randal E. Bryant, "A View from the Engine Room: Computational Support for Symbolic Model Checking" in 25 Years of Model Checking (Orna Grumberg & Helmut Veith, eds.), LNCS 5000, pp. 145-149 (2008). R. P. Kurshan, "Verification Technology Transfer" in 25 Years of Model Checking (Orna Grumberg & Helmut Veith, eds.), LNCS 5000, pp. 46-64 (2008). None.
8 Oct 2 Finite Automata. Well-posed systems: deadlock/blocking, nondeterminism. None. David L. Dill, Andreas J. Drexler, Alan J. Hu & C. Han Yang, "Protocol Verification as a Hardware Design Aid" in ICCD Proceedings, pp. 522-525 (October 1992). None.
9 Oct 7 Concurrent systems. Guarded Command Languages. Murphi and examples. Invariants. Reachable Sets by Explicit State Enumeration. Murphi package for explicit state model checking. None. None.
10 Oct 9 Examples of Symmetry and its Role in Murphi. Equilvalence Relations and Quotient Reduction. Bisimulation and Simulation. Other Methods for Reducing the State Space: System Scaling and Nondeterminism. Wikipedia entries for equivalence relation, simulation and bisimulation. C. Norris Ip & David L. Dill, "Better Verification through Symmetry" in International Conference on Computer Hardware Description Languages, pp 87-100 (April 1993) John C. Mitchell, Mark Mitchell, & Ulrich Stern, "Automated analysis of cryptographic protocols using Murphi" in IEEE Symposium on Security and Privacy, pp.141-151 (May 1997). C. Norris Ip & David L. Dill, "Better Verification through Symmetry" in Formal Methods in System Design, Volume 9, Numbers 1/2, pp 41-75 (August 1996) -- This is the long, formal and precise version of the required paper.
11 Oct 14 Continuous and Hybrid Dynamical Systems. Interactive Education Modules in Scientific Computing: Ordinary Differential Equations (online material for Heath's book). John Polking's pplane software for phase plane plots of ODEs. Lygeros notes chapters 1, 2. Lygeros citations.
12 Oct 16 Well-posed Differential Equations. Hybrid Time Trajectories. Hybrid Trajectories and Executions. Classes of Hybrid Systems. Well-posed Hybrid Systems. Wiki page collecting tools for hybrid systems (both simulation and verification). Lygeros notes chapter 3, 4 Lygeros citations.
13 Oct 21 Reachability Algorithms for Continuous Systems: Lagrangian Schemes with Polytopes and Zonotopes. Lecture slides for both lecture 13 & 14 (4.7 MB). CheckMate. MATISSE. PHAVer. d/dt. Alongkrit Chutinan & Bruce H. Krogh, "Computing polyhedral approximations to flow pipes for dynamic systems" in Proceedings of IEEE International Conference on Decision and Control (Tampa, FL), pp. 2089-2094 (1998). Antoine Girard, "Reachability of Uncertain Linear Systems Using Zonotopes" in Hybrid Systems Computation & Control (Manfred Morari & Lothar Thiele eds), LNCS 3414, pp. 291-305 (2005). Alongkrit Chutinan & Bruce H. Krogh, "Computational techniques for hybrid system verification" in IEEE Transactions on Automatic Control, vol. 48, num. 1, pp. 64-75 (2003). Eugene Asarin, Olivier Bournez, Thao Dang & Oded Maler, "Approximate Reachability Analysis of Piecewise-Linear Dynamical Systems" in Hybrid Systems Computation & Control (Nancy Lynch & Bruce H. Krogh eds.), LNCS 1790, pp. 20-31 (2000). Eugene Asarin, Thao Dang, Goran Frehse, Antoine Girard, Colas Le Guernic & Oded Maler, "Recent Progress in Continuous and Hybrid Reachability Analysis" in IEEE International Symposium on Computer-Aided Control Systems Design (Munich, Germany), pp. 1582-1587 (2006).
14 Oct 23 Reachability Algorithms for Continuous Systems: Lagrangian Schemes with Ellipsoids and Projectagons. Lecture slides for both lecture 13 & 14 (4.7 MB). Ellipsoidal Toolbox. Alexander B. Kurzhanski & Pravin Varaiya, "Ellipsoidal Techniques for Reachability Analysis" in Hybrid Systems Computation & Control (Nancy Lynch & Bruce H. Krogh eds.), LNCS 1790, pp. 202-214 (2000). Mark R. Greenstreet & Ian Mitchell, "Reachability Analysis Using Polygonal Projections" in Hybrid Systems Computation & Control (Frits W. Vaandrager & Jan H. van Schuppen, eds.), LNCS 1569, pp. 103-116 (1999). Alex A. Kurzhanskiy & Pravin Varaiya, "Ellipsoidal Toolbox (ET)" in Proceedings of IEEE International Conference on Decision and Control (San Diego, CA), pp. 1498-1503 (2006). Oleg Botchkarev & Stavros Tripakis, "Verification of Hybrid Systems with Linear Differential Inclusions Using Ellipsoidal Approximations" in Hybrid Systems Computation & Control (Nancy Lynch & Bruce H. Krogh eds.), LNCS 1790, pp. 73-88 (2000). Chao Yan & Mark R. Greenstreet, "Circuit Level Verification of a High-Speed Toggle" in Proceedings of Formal Methods in Computer Aided Design (Austin, TX), pp. 199-206 (2007).
15 Oct 28 Comparing Forward and Backward Reachability. Comparing Reachability Slides (3.6 MB). Ian M. Mitchell, "Comparing Forward & Backward Reachability as Tools for Safety Analysis" in Hybrid Systems Computation & Control (Alberto Bemporad, Antonio Bicchi & Giorgio Buttazzo eds.), LNCS 4416, pp. 428-443 (2007). None.
16 Oct 30 Reachable Sets for Nonlinear Systems with Inputs: Eulerian Schemes using Hamilton-Jacobi and Viability Methods. Eulerian Reachability slides (3.2 MB). The Toolbox of Level Set Methods. Claire J. Tomlin, Ian M. Mitchell, Alexandre M. Bayen & Meeko Oishi, "Computational Techniques for the Verification of Hybrid Systems" in Proceedings of the IEEE, volume 91, number 7, pp. 986-1001 (July 2003). Lygeros notes chapter 7. Ian M. Mitchell, Alexandre M. Bayen & Claire J. Tomlin, "A Time-Dependent Hamilton-Jacobi Formulation of Reachable Sets for Continuous Dynamic Games" in IEEE Transactions on Automatic Control, volume 50, number 7, pp. 947-957 (July 2005).
17 Nov 4 Revisiting quotient transition systems, simulation and bisimulation. Timed Automata. None. Lygeros notes chapter 6. Rajeev Alur & David L. Dill, "A Theory of Timed Automata" in Theoretical Computer Science, vol. 126, num. 2, pp. 183-235 (1994). Rajeev Alur, Thomas A. Henzinger, Gerardo Lafferriere & George J. Pappas, "Discrete Abstractions of Hybrid Systems" in Proceedings of the IEEE, vol. 88, num. 7, pp. 971-984 (2000).
18 Nov 6 Barrier Certificates. Invariant sets. Stability. None. Stephen Prajna & Ali Jadbabaie, "Safety Verification of Hybrid Systems Using Barrier Certificates" in Hybrid Systems Computation & Control (Rajeev Alur & George J. Pappas, eds.), LNCS 2993, pp. 477-492 (2004). Lygeros citations in chapter 5. Stephen Prajna, Ali Jadbabaie, & George J. Pappas, "A Framework for Worst-Case and Stochastic Safety Verification Using Barrier Certificates" in IEEE Transactions on Automatic Control, volume 52, number 8, pp. 1415-1428 (2007).
Nov 11 Remembrance Day. No Lecture.
19 Nov 13 Lyapunov Functions. Wikipedia entries for Lyapunov stability, Lyapunov function, control Lyapunov function, Krasovskii-LaSalle invariance principle and Aleksandr Mikhailovich Lyapunov. Michael Branicky, "Multiple Lyapunov Functions and Other Analysis Tools for Switched and Hybrid Systems" in IEEE Transactions on Automatic Control, volume 42, number 4, pp. 475-482 (1998) [We will only discuss Multiple Lyapunov Functions (essentially sections 1 & 2] None.
20 Nov 18 Temporal Logics: CTL, LTL and CTL*. None. E. M. Clarke, E. A. Emerson & A. P. Sistla, "Automatic Verification of Finite-State Concurrent Systems using Temporal Logic Specifications" in ACM Trans. Programming Languages, volume 8, number 2, pp. 244-263 (April 1986). We will not go into the details of the alternating bit protocol. E. Allen Emerson & Joseph Y. Halpern, "'Sometimes' and 'Not Never' Revisited: On Branching versus Linear Time Temporal Logic" in Journal of the ACM, volume 33, number 1, pp. 151-178 (January 1986). A discussion of differences between CTL, CTL* and LTL.
21 Nov 20 Model Checking CTL. None. None. None.
22 Nov 25 Fairness and CTL. Safety vs Liveness. BDD Reachability. SMV. SMV package for CTL model checking. Alan J. Hu, "Formal Hardware Verification with BDDs: An Introduction" in IEEE Pacific Rim Conference on Communications, Computers and Signal Processing, pp. 677-682 (August 1997). O. Coudert and J. C. Madre, "A Unified Framework for the Formal Verification of Sequential Circuits" in Proceedings of ICCAD pp. 126-129 (November 1990). H. J. Touati, H. Savoj, B. Lin, R. K. Brayton, and A. Sangiovanni-Vincentelli, "Implicit State Enumercation of Finite State Machines using BDD's" in Proceedings of ICCAD pp. 130-133 (November 1990)
23 Nov 27 A brief example of software verification: the SLAM toolkit. SLAM toolkit, specifically developed for Windows device driver verification, but can be generalized. Mike Hinchey et al, "Software Engineering and Formal Methods", Communications of the ACM, vol. 51, num. 9, pp. 54-59 (September 2008). Thomas Ball & Sriram K. Rajamani, "Automatically Validating Temporal Safety Properties of Interfaces", Proc. SPIN Workshop on Model Checking of Software, pp. 103-122 (2001). Citations from the Hinchey paper on termination proofs and Astree. Flanagan et al, "Extended Static Checking for Java", Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 234-245 (2002).
Dec 3-17 Exam Period. Project presentations Thursday December 4, ICICS 238, 14:00 - 15:30. Final report due Friday December 19 at noon.

Links:

CS 513 Term 1 Winter 2008-2009 Class Page
maintained by Ian Mitchell