!!! This class has been cancelled !!!

Computer-Aided Formal Methods

Course number: COEN 396.  Section: 31189.

Time: Tue 7:10-9:00 PM.  Start: 1 April 2003.  Location: TBA

Instructor:  Ching-Tsun Chou

Course Description

The need for gaining confidence through mathematical reasoning in the correctness of various aspects of a complex computer system (circuits, protocols, programs, …) has been recognized since the dawn of computing.  For instance, in a fascinating paper published in 1949, Alan Turing gave a correctness proof (including termination) of a factorial program with two loops.  While pencil-and-paper proofs and “thinking things through carefully” in general can be very helpful, techniques relying on the unaided brain alone cannot be scaled up to cope with many of the complex hardware and software algorithms used in modern computer systems.  Formal methods are not practically useful until they are at least partially automated.

This course is an overview of some of the automated and semi-automated formal methods (e.g., binary decision diagrams, boolean satisfiability checking, symbolic trajectory evaluation, symbolic and explicit-state model checking, mechanical theorem proving) and some of their successful industrial applications (e.g., circuit equivalence checking, verification of cache coherence and other protocols, verification of floating-point hardware and algorithms).  After taking this course, a student should be able to understand the basic concepts and techniques of computer-aided formal methods, know what such techniques are and are not good for, and have a sense of which techniques and tools might be most useful when faced with a real-world verification problem.  The emphasis of this course is not on theory (though the necessary theoretical background will be covered), but on hands-on experience.  Each student is expected to play with at least one of the formal verification tools listed below and write a report about his or her experience.

Course Contents

Format and Grading

One 2-hour lecture per week for 10 weeks, two homework assignments, and one final report.  The instructor will assign problems to solve for the homeworks.  The students are expected to propose their own projects for the final report (subject to the instructor’s approval).  The number of students will decide whether the students will do the final report projects individually or in small groups.  There is no final exam, whose time will be used for the students to present the results of their projects.  The grading is roughly 40% homework assignments, 40% final report, and 20% class attendance and participation.  The instructor may adjust these percentages at his discretion.

Computing Requirements

Linux is the preferred computing platform, since all tools listed below should run on it.  Some of the tools also run on Windows and some on other Unix platforms as well.  Each student should download and test his or her chosen tool for the final report as soon as possible, as one never knows what may go wrong when installing software on supposedly standard platforms.

Office hours

One hour before each class.  The place is to be decided.  The instructor can also be reached via email at ching-tsun.chou@intel.com.

Lecture notes

The instructor will make the lecture notes available on the web when they are ready.  Much of the reading materials are research papers, almost all of which are available on the web.  Several tools listed below come with excellent documentation, in particular Forte and Cadence SMV, from which the instructor plans to lecture.  There are also several similar courses offered at other educational institutions available on the web.

Textbooks

None required, though some students may find it a good idea to get one of the following books in order to have something definite to refer to.  They cover similar sets of topics to various depths, though none of them covers exactly the same materials covered in this course.  The instructor will bring copies of them to the class so that each student can decide which one(s) best suits his or her taste.

Syllabus

Tentative, especially the times of the guest lectures.

 

Course Resources

Tools

All tools listed below should be free for academic purposes.

 

Courses

Other similar courses on the web.

Papers

If no URL is given or the given URL does not work, try Google (http://www.google.com/) or CiteSeer (http://citeseer.nj.nec.com/cs).

 

  1. Henrik Reif Andersen, "An Introduction to Binary Decision Diagrams", lecture notes, 1998.  (http://www.itu.dk/people/hra/notes-index.html)
  2. A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu, "Symbolic Model Checking without BDDs", Tools and Algorithms for the Analysis and Construction of Systems (TACAS'99), LNCS Vol. 1579.  (http://www-2.cs.cmu.edu/~modelcheck/ed-papers/SMCwBDDS.pdf)
  3. Karl S. Brace, Richard L. Rudell, and Randal E. Bryant, "Efficient Implementation of a BDD Package", 27th Design Automation Conference, pp. 40-45, 1990.  (http://delivery.acm.org/10.1145/130000/123222/p40-brace.pdf?key1=123222&key2=8212355401&coll=portal&dl=ACM&CFID=7873006&CFTOKEN=85130598)
  4. R. E. Bryant, ``Graph-Based Algorithms for Boolean Function Manipulation,'' IEEE Transactions on Computers, Vol. C-35, No. 8 (August, 1986), pp. 677-691.  (http://www.cs.cmu.edu/~bryant/pubdir/ieeetc86.ps)
  5. R. E. Bryant, ``On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Application to Integer Multiplication,'' IEEE Transactions on Computers, Vol. 40, No. 2 (February, 1991), pp. 205-213.  (http://www.cs.cmu.edu/~bryant/pubdir/ieeetc91.ps)
  6. J.R. Burch, E.M. Clarke, D.E. Long, K.L. McMillan, D.L. Dill, “Symbolic Model Checking for Sequential Circuit Verification”, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 13(4):401–424, 1994.  (http://citeseer.nj.nec.com/burch93symbolic.html)
  7. Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, L. J. Hwang, “Symbolic Model Checking: 10^20 States and Beyond”, Information and Computation 98(2): 142-170, 1992.  (http://www-2.cs.cmu.edu/~emc/15-820A/reading/burch90symbolic.pdf)
  8. E.M. Clarke, E.A. Emerson, A.P. Sistla, “Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specification”, ACM Transactions on Programming Languages and Systems, Vol. 8, No. 2, April 1986, Pages 244-263.  (http://www-2.cs.cmu.edu/~emc/15-820A/reading/p244-clarke.pdf)
  9. Edmund M. Clarke and Robert P. Kurshan, "Computer-Aided Verification", IEEE Spectrum, June 1996, pp. 61-67.
  10. David L. Dill, Andreas J. Drexler, Alan J. Hu, and C. Han Yang, "Protocol Verification as a Hardware Design Aid", International Conference on Computer Design, 1992.  (http://sprout.stanford.edu/dill/PAPERS/verification/DDHY92.ps)
  11. J. Gu, P. Purdom, J. Franco, and B. Wah, “Algorithms for the Satisfiability (SAT) Problem: a Survey”, preliminary version, 1996.  (http://citeseer.nj.nec.com/56722.html)
  12. Alan J. Hu, "Formal Hardware Verification with BDDs: An Introduction", IEEE Pacific Rim Conference on Communications, Computers, and Signal Processing (PACRIM'97), 1997.  (http://www.cs.ubc.ca/spider/ajh/mypapers/97H1.ps.gz)
  13. C. Norris Ip and David L. Dill, “Better Verification through Symmetry”, Formal Methods in System Design, Volume 9, Numbers 1/2, pp 41-75, August 1996.  (http://sprout.stanford.edu/PAPERS/ID96B.ps)
  14. Kenneth L. McMillan, Symbolic Model Checking, CMU-CS-92-131, May 1992.  (http://www-cad.eecs.berkeley.edu/~kenmcmil/thesis.ps)
  15. Joćo P. Marques-Silva and Karem A. Sakallah, "GRASP -- A New Search Algorithm for Satisfiability," in Proceedings of IEEE/ACM International Conference on Computer-Aided Design, November 1996.  (http://sat.inesc.pt/~jpms/research/papers/iccad96/iccad96.ps.gz)
  16. John Moondanos, Carl-Johan H. Seger, Ziyad Hanna, Daher Kaiss, “CLEVER: Divide and Conquer Combinational Logic Equivalence Verification with False Negative Elimination”, Computr Aided Verification (CAV) 2001, pp.131-143.
  17. M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, S. Malik, “Chaff: Engineering an Efficient SAT Solver”, 39th Design Automation Conference, Las Vegas, June 2001.  (http://www.ee.princeton.edu/~chaff/publication/DAC2001v56.pdf)
  18. J. O’Leary, X. Zhao, R, Gerth, C.-J. H. Seger, “Formally Verifying IEEE Compliance of Floating-Point Hardware”, Intel Technology Journal, 1st Quarter, 1999.  (http://www.intel.com/technology/itj/q11999/articles/art_5.htm)
  19. C.-J. H. Seger, and R. E. Bryant, ``Formal Verification by Symbolic Evaluation of Partially-Ordered Trajectories,'' Formal Methods in System Design, Vol. 6, No. 2 (March, 1995), pp. 147-190.  Preprint (http://www.cs.cmu.edu/~bryant/pubdir/fmsd95.ps)
  20. Ulrich Stern and David L. Dill, “Improved probabilistic verification by hash compaction”, Correct Hardware Design and Verification Methods: IFIP WG10.5 Advanced Research Working Conference Proceedings, 1995.  (http://sprout.stanford.edu/dill/PAPERS/verification/SD95A.ps)
  21. U. Stern and D. L. Dill. A New Scheme for Memory-Efficient Probabilistic Verification, Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification, pages 333-48, 1996.  (http://sprout.stanford.edu/dill/PAPERS/verification/SD96A.ps)
  22. A.M. Turing, “Checking a Large Routine”. Paper for the EDSAC Inaugural Conference, 24 June 1949. Typescript published in Report of a Conference on High Speed Automatic Calculating machines, pp.67-69.  Reprinted with corrections and annotations in “An early program proof by Alan Turing”, by L. Morris and C. B. Jones, Annals of the History of Computing, 6 (2) pp.129-143 (1984).

About the Instructor

Ching-Tsun Chou is a Platform Architect and Verification Engineer at Intel Corporation, where he applies formal methods to the design, definition, and verification of complex protocols used in distributed shared memory systems.  Earlier he was a Verification Engineer in Intel’s Itanium™ processor design team, where worked on both formal and simulation-based hardware verification, and a VLSI CAD Researcher in Fujitsu Labs of America, where he worked on the application of synchronous programming languages to hardware design.  He has published a number of papers on formal verification, synchronous programming, and distributed algorithms and served on the program committees of several international conferences on formal verification.  He earned a Ph.D. degree in Computer Science from UCLA and has one patent pending.  His CV is available at http://home.pacbell.net/ctchou/ctchou-resume.html

Last modified:  7 April 2003

!!! This class has been cancelled !!!