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

Instructor: Marius Minea

marius@cs.upt.ro

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**

- 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

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.

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.

An excellent survey for the topics in the first part of the course.

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

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