Faculty of Information Technology, BUT

Course details

Formal Program Analysis

FAD Acad. year 2009/2010 Winter semester

An overview of various methods of analysis and verification of programs with formal roots. Model checking of finite-state systems: the basic principles, specification of properties to be verified, temporal logics, the state explosion problem and existing approaches to solving it (esp. partial order reduction and symbolic verification based on binary decision diagrams). Predicate abstraction. Various ways of static analysis, dataflow analyses, bug pattern analyses, abstract interpretation. SAT solving and SMT solving. Dynamic analyses.

Guarantor

Language of instruction

Czech

Completion

Examination (oral)

Time span

26 hrs lectures

Assessment points

100 exam

Department

Subject specific learning outcomes and competences

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.

Generic learning outcomes and competences

A deeper ability to read and create formal texts.

Learning objectives

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.

Prerequisite kwnowledge and skills

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

Study literature

  • Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking, MIT Press, 2000. ISBN 0-262-03270-8
  • Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis, Springer-Verlag, 2005. ISBN 3-540-65410-0

Fundamental literature

  • 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.

Syllabus of lectures

  1. An overview of the existing methods of formal analysis and verification of programs, their possibilities, advantages and disadvantages.
  2. Temporal logics CTL, LTL, and CTL*.
  3. Explicit-state CTL* model checking.
  4. The state explosion problem and possibilities of fighting it. Partial order reduction.
  5. Binary decision diagrams (BDDs).
  6. Symbolic verification based on BDDs.
  7. The automata-theoretic approach to LTL model checking.
  8. Automated abstraction with a stress on predicate abstraction, Craig interpolants.
  9. SAT solving, SMT solving.
  10. Classical dataflow analyses (such as live variables, available expressions, etc.) as well as some selected, more advanced dataflow analyses (like some pointer analyses).
  11. A note on abstract interpretation.
  12. Static analyses based on searching for bug patterns.
  13. Dynamic analyses.

Syllabus - others, projects and individual work of students

  1. To read and understand a state-of-the-art research paper (or papers) from the area of model checking, theorem proving, static or dynamic analysis and to write a report based on the paper (papers) read.

Progress assessment

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

Controlled instruction

Lectures and a preparation of a report.

Course inclusion in study plans

Back to top