Course detail

Formal Program Analysis

FIT-FADAcad. year: 2017/2018

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, efficient storage of state spaces, state space reductions, modular verification, automated abstraction (with a stress on predicate abstraction that plays a key role in software model checking). Model checking of infinite-state systems: cut-offs, symbolic model checking, abstraction, automated induction. Theorem proving, SAT solving, SMT solving. Various ways of static analysis, dataflow analysis, constraint-based analysis, type analysis, metacompilation, abstract interpretation. Dynamic analysis with a formal basis, algorithms like Eraser or Daikon, applications automated inference methods in dynamic analysis.

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

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

Study evaluation is based on marks obtained for specified items. Minimimum number of marks to pass is 50.

Course curriculum

    Syllabus of lectures:
    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.

    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.

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

Not applicable.

Recommended reading

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

Classification of course in study plans

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

Syllabus

  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.