Contents of this page

Growing Set: avi mpg Final Set: avi mpg 
#  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 
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 OverviewWhat 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:
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 subdisciplines 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:
Expectations: In addition to attending lectures, students will:

Intended Audience: Graduate students in
Prerequisites: Graduate standing or consent of the instructor.
Grades: Your final grade will be based on a combination of:
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:
#  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. 1416 (July 2008). Leah Hoffman, "Q&A: Talking Model Checking Technology" in Communications of the ACM, vol. 51, num. 7, pp. 110112 (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, "ComputerAided Verification" in IEEE Spectrum, June 1996, pp. 6167  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. 293318.  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. 4045 (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.205213 (February 1991). 
5  Sept 23  An Analog Verification Digression. Guest Lecturer Mark Greenstreet.  None.  Mark R. Greenstreet & Suwen Yang, "Verifying startup conditions for a ring oscillator" in Proceedings of the 18th ACM Great Lakes Symposium on VLSI, pp. 201206 (May 2008).  None. 
6  Sept 25  SAT Solvers and Verification. Guest Lecturer Alan J. Hu.  MiniSat, a "minimalistic opensource 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. 1736 (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. 279285. An even broader survey is Vipin Kumar, "Algorithms for Constraint Satisfaction Problems: A Survey" in AI Magazine, volume 13, number 1, pp. 3244, (1992). 
7  Sept 30  Equivalence Checking Wrapup. 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. 145149 (2008). R. P. Kurshan, "Verification Technology Transfer" in 25 Years of Model Checking (Orna Grumberg & Helmut Veith, eds.), LNCS 5000, pp. 4664 (2008).  None. 
8  Oct 2  Finite Automata. Wellposed 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. 522525 (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 87100 (April 1993)  John C. Mitchell, Mark Mitchell, & Ulrich Stern, "Automated analysis of cryptographic protocols using Murphi" in IEEE Symposium on Security and Privacy, pp.141151 (May 1997). C. Norris Ip & David L. Dill, "Better Verification through Symmetry" in Formal Methods in System Design, Volume 9, Numbers 1/2, pp 4175 (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  Wellposed Differential Equations. Hybrid Time Trajectories. Hybrid Trajectories and Executions. Classes of Hybrid Systems. Wellposed 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. 20892094 (1998). Antoine Girard, "Reachability of Uncertain Linear Systems Using Zonotopes" in Hybrid Systems Computation & Control (Manfred Morari & Lothar Thiele eds), LNCS 3414, pp. 291305 (2005).  Alongkrit Chutinan & Bruce H. Krogh, "Computational techniques for hybrid system verification" in IEEE Transactions on Automatic Control, vol. 48, num. 1, pp. 6475 (2003). Eugene Asarin, Olivier Bournez, Thao Dang & Oded Maler, "Approximate Reachability Analysis of PiecewiseLinear Dynamical Systems" in Hybrid Systems Computation & Control (Nancy Lynch & Bruce H. Krogh eds.), LNCS 1790, pp. 2031 (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 ComputerAided Control Systems Design (Munich, Germany), pp. 15821587 (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. 202214 (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. 103116 (1999).  Alex A. Kurzhanskiy & Pravin Varaiya, "Ellipsoidal Toolbox (ET)" in Proceedings of IEEE International Conference on Decision and Control (San Diego, CA), pp. 14981503 (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. 7388 (2000). Chao Yan & Mark R. Greenstreet, "Circuit Level Verification of a HighSpeed Toggle" in Proceedings of Formal Methods in Computer Aided Design (Austin, TX), pp. 199206 (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. 428443 (2007).  None. 
16  Oct 30  Reachable Sets for Nonlinear Systems with Inputs: Eulerian Schemes using HamiltonJacobi 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. 9861001 (July 2003).  Lygeros notes chapter 7. Ian M. Mitchell, Alexandre M. Bayen & Claire J. Tomlin, "A TimeDependent HamiltonJacobi Formulation of Reachable Sets for Continuous Dynamic Games" in IEEE Transactions on Automatic Control, volume 50, number 7, pp. 947957 (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. 183235 (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. 971984 (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. 477492 (2004).  Lygeros citations in chapter 5. Stephen Prajna, Ali Jadbabaie, & George J. Pappas, "A Framework for WorstCase and Stochastic Safety Verification Using Barrier Certificates" in IEEE Transactions on Automatic Control, volume 52, number 8, pp. 14151428 (2007). 
Nov 11  Remembrance Day. No Lecture.  
19  Nov 13  Lyapunov Functions.  Wikipedia entries for Lyapunov stability, Lyapunov function, control Lyapunov function, KrasovskiiLaSalle 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. 475482 (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 FiniteState Concurrent Systems using Temporal Logic Specifications" in ACM Trans. Programming Languages, volume 8, number 2, pp. 244263 (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. 151178 (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. 677682 (August 1997).  O. Coudert and J. C. Madre, "A Unified Framework for the Formal Verification of Sequential Circuits" in Proceedings of ICCAD pp. 126129 (November 1990). H. J. Touati, H. Savoj, B. Lin, R. K. Brayton, and A. SangiovanniVincentelli, "Implicit State Enumercation of Finite State Machines using BDD's" in Proceedings of ICCAD pp. 130133 (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. 5459 (September 2008). Thomas Ball & Sriram K. Rajamani, "Automatically Validating Temporal Safety Properties of Interfaces", Proc. SPIN Workshop on Model Checking of Software, pp. 103122 (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. 234245 (2002). 
Dec 317  Exam Period. Project presentations Thursday December 4, ICICS 238, 14:00  15:30. Final report due Friday December 19 at noon. 