Formal verification

Fall semester 2008/2009 (old version: 2006/2007)
Instructor: Marius Minea

Course information

Lectures: Mon 18-20h, A 109
Project: Mon 20-21h, Wed 20-21 and Fri 8-9h, B426
Office hours: on request

Projects and homeworks: 50%.
Exam: 50% (midterm upon request)

Makeup exam: Mon 19 Apr., 8am, A212
Grades Final makeup grades 2010

Lecture notes

Sample exam questions

Projects and homeworks

Project 1
Modeling and verification of a concurrent system using Spin
Handed out: Oct. 9. Due: Nov. 21
Resources: Spin/Promela manual

Project 2
Modeling and verification of a concurrent system with timing constraints using UPPAAL
Due: Jan. 16
The system functionality and the truth value of specifications should depend on timing in a nontrivial way. The model can be adapted from the previous project, or a different one.


Introductory papers

E. M. Clarke, R. P. Kurshan. "Computer Aided Verification", IEEE Spectrum, vol. 33, no. 6, pp. 61-67, iun. 1996. (PS, 6.1MB)
A history of formal verification methods in hardware, with a detailed description of several applications.

E. M. Clarke, J. M. Wing. "Formal Methods. State of the Art and Future Directions", ACM Computing Surveys, vol. 28, no. 4, pp. 626-643, dec. 1996. (PS, 188kB)
A concise definition and classification, with many application examples.

Model checking

E. Clarke, O. Grumberg, D. Long. "Verification Tools for Finite State Concurrent Systems", A Decade of Concurrency -- Reflections and Perspectives, REX School/Symposium, Noordwijkerhout, Netherlands. Lecture Notes in Computer Science, vol. 803, pp. 124-175, Springer Verlag, iun. 1993. (PS, 736kB)
An excellent survey for the topics in the first part of the course.

Binary decision diagrams

R. E. Bryant. "Graph-Based Algorithms for Boolean Function Manipulation", IEEE Transactions on Computers, vol. C-35 no. 8, pp. 677--691, aug. 1986. (PS, 384kB)
The classic article which defined BDDs (most cited article ever on CiteSeer!)

R. E. Bryant. "Binary Decision Diagrams and Beyond: Enabling Technologies for Formal Verification", International Conference on Computer Design, pp. 236--243, nov. 1995 (PS, 240kB)
A survey on BDDs and their variants


S. Bilaniuk. "A Problem Course in Mathematical Logic". Freeware text

Relations between models, compositionality, abstraction

E. Clarke, O. Grumberg, D. Long. "Model checking", Proceedings of the International Summer School on Deductive Program Design Marktobedorf, Germany, 1994. In M. Broy, "Deductive Program Design", NATO ASI Series F vol. 152, Springer Verlag, 1996. (PS, 438 kB)
Most of the material in lecture 11.

H. Peng, S. Tahar. "A Survey on Compositional Verification", Technical Report, Concordia University, Canada, Department of Electrical and Computer Engineering, dec. 1998. (PS, 475 kB)
An elementary introduction

Marius Minea
Last modified: Mon Oct 15 18:05:26 EET 2007