Course detail

Formal Program Analysis

FIT-FADAcad. year: 2021/2022

An overview of various methods of analysis and verification of programs with formal roots. Model checking: basic principles, specification of properties to be verified, temporal logics, the state explosion problem and existing approaches to solving it, binary decision diagrams, automated abstraction (with a stress on predicate abstraction that plays a key role in software model checking). Various approaches to static analysis: dataflow analysis, pointer analyses, constraint-based analysis, type analysis, abstract interpretation. Deductive verification, SAT solving, SMT solving, symbolic execution. Dynamic analysis with a formal basis, algorithms like FastTrack or dynamic partial order reduction.

Areas for the Doctoral State Exam:

1. Temporal logics LTL, CTL, and CTL*.
2. Büchi automata and LTL model checking based on them.
3. CTL model checking.
4. Binary decision diagrams.
5. Predicate abstraction.
6. Abstract interpretation.
7. Data-flow analysis.
8. SAT solving and SMT solving.
9. Symbolic execution.
10. Deductive verification.

Language of instruction

Czech

Mode of study

Not applicable.

Guarantor

prof. Ing. Tomáš Vojnar, Ph.D.

Department

Department of Intelligent Systems (UITS)

Learning outcomes of the course unit

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.

Prerequisites

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

Co-requisites

Not applicable.

Planned learning activities and teaching methods

Not applicable.

Assesment methods and criteria linked to learning outcomes

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

Course curriculum

Not applicable.

Work placements

Not applicable.

Aims

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.

Specification of controlled education, way of implementation and compensation for absences

Lectures and a preparation of a report.

Recommended optional programme components

Not applicable.

Prerequisites and corequisites

Not applicable.

Basic literature

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 
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking, MIT Press, 2000. ISBN 0-262-03270-8 
Monin, J.F., Hinchey, M.G.: Understanding Formal Methods, Springer-Verlag, 2003. ISBN 1-852-33247-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. 
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 

Recommended reading

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.)
Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, 2008.
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.
Bradley, A.R., Manna, Z.: The Calculus of Computation: Decision Procedures with Applications to Verification, Springer, 2007.
Clarke, E.M., Henzinger, Th.A., Veith, H., Bloem, R. (Eds.): Handbook of Model Checking, Springer International Publishing, 2018.
Edmund, M.C., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, 2000.
Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual, Addison-Wesley Professional, 2003.
Chess, B., West,J.: Secure Programming with Static Analysis. Addison-Wesley Professional, 2007.
Khedker, U., Sanyal, A., Sathe, B.: Data Flow Analysis: Theory and Practice, CRC Press, 2009.
Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View, Springer, 2008.
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.
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.
Rival, X., Yi, K.: Introduction to Static Analysis. An Abstract Interpretation Perspective. MIT Press, 2020.
Soubor materiálů prezentovaných na přednáškách a zveřejněných přes WWW.
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.

Classification of course in study plans

  • Programme DIT Doctoral 0 year of study, winter semester, compulsory-optional
  • Programme DIT Doctoral 0 year of study, winter semester, compulsory-optional

  • Programme CSE-PHD-4 Doctoral

    branch DVI4 , 0 year of study, winter semester, elective

  • Programme CSE-PHD-4 Doctoral

    branch DVI4 , 0 year of study, winter semester, elective

  • Programme DIT-EN Doctoral 0 year of study, winter semester, compulsory-optional
  • Programme DIT-EN Doctoral 0 year of study, winter semester, compulsory-optional

  • Programme CSE-PHD-4 Doctoral

    branch DVI4 , 0 year of study, winter semester, elective

  • Programme CSE-PHD-4 Doctoral

    branch DVI4 , 0 year of study, winter semester, elective

Type of course unit

 

Lecture

26 hod., optionally

Teacher / Lecturer

prof. Ing. Tomáš Vojnar, Ph.D.
Ing. Ondřej Lengál, Ph.D.

Syllabus

  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.

Guided consultation in combined form of studies

26 hod., optionally

Teacher / Lecturer

prof. Ing. Tomáš Vojnar, Ph.D.