Formal Program Analysis

• 26 hrs lectures

• 100 pts final exam

Acquaintance with possibilities, limitations, and principles of the state-of-the-art methods of program analysis on a formal basis. Ability to apply them in advanced projects and an overall knowledge of the way these techniques can evolve in the future.
A deeper ability to read and create formal texts.

The goal of the course is to acquaint the students with principles, possibilities, and restrictions of the currently most successful methods known, resp. being studied, in the area of applying formal methods for an automated analysis and verification of programs.

Acquaintance with basics of logics, algebra, graph theory, theory of formal languages and automata, compilers, and computability and complexity.

• Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking, MIT Press, 2000. ISBN 0-262-03270-8
• Berard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P., McKenzie, P.: Systems and Software Verification: Model-Checking Techniques and Tools, Springer-Verlag, 2001. ISBN 3-540-41523-8
• Monin, J.F., Hinchey, M.G.: Understanding Formal Methods, Springer-Verlag, 2003. ISBN 1-852-33247-6
• Valmari, A.: The State Explosion Problem. In Reisig, W., Rozenberg, G.: Lectures on Petri Nets I: Basic Models, Lecture Notes in Computer Science, č.1491, s. 429-528. Springer-Verlag, 1998. ISBN 3-540-65306-6
• Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis, Springer-Verlag, 2005. ISBN 3-540-65410-0
• Schwartzbach, M.I.: Lecture Notes on Static Analysis, BRICS, Department of Computer Science, University of Aarhus, Denmark, 2006.

1. An overview of the existing methods of formal analysis and verification of programs, their possibilities, advantages and disadvantages.
2. Model checking of finite-state systems: the basic principle, specification of properties to be checked, temporal logics.
3. The state explosion problem and possibilities of fighting it, efficient state space storage, state space reduction.
4. Modular verification, automated abstraction with a stress on predicate abstraction, Craig interpolants.
5. Model checking of infinite-state systems: cut-offs, symbolic verification, abstraction, automated induction.
6. Theorem proving.
7. SAT solving, SMT solving.
8. Static analysis based on dataflow analysis.
9. Constraint-based static analysis.
10. Type analysis.
11. Metacompilation.
12. Abstract interpretation.
13. Dynamic analysis on a formal basis, algorithms like Eraser and Daikon, using automated inference methods in dynamic analysis.

Discussions within the lectures, a check of the prepared report.

Lectures and a preparation of a report.