Formal verification

Fall semester 2008/2009 (old version: 2006/2007)
Instructor: Marius Minea
marius@cs.upt.ro

Course information

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

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

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

Lecture notes

Introduction to Formal Methods PDF, 1:1 1:6, for printing
Elements of Mathematical Logic PDF, 1:1 1:6, for printing
Applications: formalising in predicate logic, resolution, unification (Gordon Novak, U. of Texas at Austin)
Model Checking Basics PDF, 1:1 1:6, for printing
Symbolic Model Checking PDF, 1:1 1:6, for printing
Verification of Timed Systems PDF, 1:1 1:6, for printing (only introduction and timed automata)
Program semantics, analysis and verification PDF, 1:1 1:6, for printing (up to predicate abstraction)
Comparing models. PDF, 1:1 1:6, for printing (slides 1-10)
Model checking with automata. PDF, 1:1 1:6, for printing (slides 13-18)
Software verification with preficate abstraction PDF, 1:1 1:6, for printing (slides 15-24)
Static analysis PDF, 1:1 1:6, for printing (suggested alternative here and here)
Abstraction. PDF, 1:1 1:6, for printing (slides 11-18)
Verification of security protocols. PDF, 1:1 1:6, for printing

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.

References

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

Logic

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