Formal Program Analysis

• 26 hrs lectures

• 70 pts final exam
• 30 pts projects

Acquaintance with possibilities, limitations, and principles of state-of-the-art methods of program analysis on a formal basis. Ability to apply them in advanced projects and 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 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.

• Bradley, A.R., Manna, Z.: The Calculus of Computation: Decision Procedures with Applications to Verification, Springer, 2007.
• Aho, A.V., Lam, S., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison Wesley, 2nd ed., 2006. (Část věnovaná statické analýze.)
• Valmari, A.: The State Explosion Problem. In Reisig, W., Rozenberg, G.: Lectures on Petri Nets I: Basic Models, volume 1491 of Lecture Notes in Computer Science, pages 429-528. Springer-Verlag, 1998.
• Chess, B., West,J.: Secure Programming with Static Analysis. Addison-Wesley Professional, 2007.
• Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View, Springer, 2008.
• Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual, Addison-Wesley Professional, 2003.
• Ben-Ari, M.: Principles of the Spin Model Checker, Springer, 2008.
• Bertot Y., Castéran, P.: Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions, Springer, 2010.
• Soubor materiálů prezentovaných na přednáškách a zveřejněných přes WWW.
• Clarke, E.M., Henzinger, Th.A., Veith, H., Bloem, R. (Eds.): Handbook of Model Checking, Springer International Publishing, 2018.
• Materiály aktuálně volně dostupné na Internetu, a to zejména články a dokumentace týkající se počítačových nástrojů pro formální analýzu a verifikaci.
• Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, 2008.
• Rival, X., Yi, K.: Introduction to Static Analysis. An Abstract Interpretation Perspective. MIT Press, 2020.
• Moller, A., Schwartzbach, M.I.: Static Program Analysis, Department of Computer Science, Aarhus University, Denmark, 2018.
• Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis, Springer-Verlag, 2005.
• Edmund, M.C., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, 2000.
• Khedker, U., Sanyal, A., Sathe, B.: Data Flow Analysis: Theory and Practice, CRC Press, 2009.

• 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 existing methods of formal analysis and verification of programs, their capabilities, advantages and disadvantages.
2. Model checking: basic principles, specification of properties to be checked, temporal logics.
3. LTL model checking based on automata.
4. The state explosion problem and possibilities of fighting it, efficient state space storage, binary decision diagrams.
5. State space reductions, especially the partial-order reduction.
6. Automated abstraction with a stress on predicate abstraction, Craig interpolants.
7. Symbolic execution.
8. Deductive verification.
9. SAT solving, SMT solving.
10. Static analysis based on dataflow analysis, pointer analyses.
11. Constraint-based static analysis, type analysis.
12. Abstract interpretation.
13. Dynamic analysis on a formal basis, algorithms like FastTrack, dynamic partial-order reduction.

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

Lectures and a preparation of a report.