Course detail

Formal Analysis and Verification

FIT-FAVAcad. year: 2017/2018

Formal analysis and verification as a modern complement and/or alternative to validating properties of systems by means of simulation or testing. Selected formalisms for specifying properties to be checked. Model checking: formal verification based on a systematic state space exploration.  Various approaches to state space reductions, especially the partial order reduction. Methods of automated abstraction of systems being examined, especially predicate abstraction. Modern methods of SAT and SMT solving and their aplications in formal analysis and verification. Static analysis based on looking for error patterns, data flow analysis, and abstract interpretation. A brief description of several advanced computer-aided tools for formal analysis and verification: SMV, Spin, Slam, Blast, Java PathFinder, ARMC, FindBugs, etc. (according to the current state of the art).

Language of instruction

Czech

Number of ECTS credits

5

Mode of study

Not applicable.

Guarantor

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

Department

Department of Intelligent Systems (UITS)

Learning outcomes of the course unit

Students are acquainted with principles and methods of formal analysis and verification and with their application within the process of designing safety-critical systems. Students know capabilities and the basic ways of using computer-aided tools for formal analysis and verification.

Acquired knowledge about the significance and possibilities of using formal methods within the development of various kinds of systems and about their growing use in practice.

Prerequisites

Knowledge of discrete mathematics, the theory of formal languages, and algorithmics on the bachelor's level is assumed.

Co-requisites

Not applicable.

Planned learning activities and teaching methods

Not applicable.

Assesment methods and criteria linked to learning outcomes

Having at least 50% of the possible point evaluation of the project.

Course curriculum

    Syllabus of lectures:
    1. The meaning of the terms ``formal analysis and verification''. Capabilities and advantages of methods of formal analysis and verification. Various approaches to formal analysis and verification: model checking, static analysis, and theorem proving.
    2. State spaces, state space paths, abstractions of states and transitions. Interleaving and true concurrency. Linear and branching time. Safety, liveness, and fairness.
    3. Temporal logics CTL and CTL*, model checking systems whose properties are specified in CTL or CTL* using explicitly represented state spaces.
    4. Binary decision diagrams for a compact, symbolic representation of state spaces and their implementation.
    5. Lattices, fix points, and the Knaster-Tarski theorem as a formal basis for symbolic model checking.
    6. Symbolic model checking for CTL and CTL*.
    7. The temporal logic LTL, the correspondence between Büchi automata and LTL formulae, model checking systems whose properties are specified in LTL using Büchi automata.
    8. The partial order state space reduction. The symmetry state space reduction. An overview of other state space reduction methods. Compositional verification.
    9. Methods of automated abstraction of systems, the predicate abstraction, the counter-example guided abstraction refinement loop, Craig interpolation.
    10. Decision procedures and modern methods of SAT and SMT solving and their use in formal verification (e.g., in the predicate abstraction).
    11. Classical dataflow analyses (such as live variables, available expressions, etc.) as well as some selected, more advanced dataflow analyses (like some pointer analyses), their description via flow equations, and iterative methods of solving these methods.
    12. Abstract interpretation and its use for defining static analyses.
    13. Static analyses based on searching for bug patterns, a note on selected dynamic analyses, esp. those for detecting concurrency-related errors.

    Syllabus - others, projects and individual work of students:
    • A project including an installation of a selected tool for automated verification on a formal basis (Spin, Blast, ARMC, SMV, JPF, FindBugs, Invader, Uppaal aj.), experiments with this tool, and a preparation of an essay describing principles on which the chosen tool is built (10 pts.) and the performed experiments (10 pts. for experiments with existing case studies, 10 pts. for new case studies). It is possible to agree on studying a tool based on principles that are not a part of the lectures (theorem proving, real-time systems, etc.).

Work placements

Not applicable.

Aims

The goal of the course is to introduce formal analysis and verification to students as a modern and promising  method of automated evaluation of properties of various kinds of safety-critical systems (such as drivers and other parts of operating systems, control software, workflow, communication protocols, parts of hardware, etc.). The course acquaints students both with the theoretical background of the given area, with computer-aided tools based on them as well as with successful applications of formal analysis and verification in practice (Microsoft, Intel, Nasa, Airbus, ...).

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

  • An evaluated project for 30 points.
  • A final examination for 70 points.
  • To be allowed to sit for the written examination, a student is to earn at least 15 points during the semester.

Recommended optional programme components

Not applicable.

Prerequisites and corequisites

Not applicable.

Basic literature

Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, 2008. 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.

Recommended reading

Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, 2008. 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. 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.) Bradley, A.R., Manna, Z.: The Calculus of Computation: Decision Procedures with Applications to Verification, Springer, 2007. 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. 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. 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. 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.

Classification of course in study plans

  • Programme IT-MSC-2 Master's

    branch MMI , 0 year of study, winter semester, elective
    branch MBI , 0 year of study, winter semester, elective
    branch MSK , 2 year of study, winter semester, compulsory-optional
    branch MMM , 0 year of study, winter semester, compulsory
    branch MBS , 0 year of study, winter semester, compulsory-optional
    branch MPV , 0 year of study, winter semester, elective
    branch MIS , 0 year of study, winter semester, compulsory-optional
    branch MIN , 0 year of study, winter semester, compulsory-optional
    branch MGM , 0 year of study, winter semester, elective

Type of course unit

 

Lecture

39 hod., optionally

Teacher / Lecturer

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

Syllabus

  1. The meaning of the terms ``formal analysis and verification''. Capabilities and advantages of methods of formal analysis and verification. Various approaches to formal analysis and verification: model checking, static analysis, and theorem proving.
  2. State spaces, state space paths, abstractions of states and transitions. Interleaving and true concurrency. Linear and branching time. Safety, liveness, and fairness.
  3. Temporal logics CTL and CTL*, model checking systems whose properties are specified in CTL or CTL* using explicitly represented state spaces.
  4. Binary decision diagrams for a compact, symbolic representation of state spaces and their implementation.
  5. Lattices, fix points, and the Knaster-Tarski theorem as a formal basis for symbolic model checking.
  6. Symbolic model checking for CTL and CTL*.
  7. The temporal logic LTL, the correspondence between Büchi automata and LTL formulae, model checking systems whose properties are specified in LTL using Büchi automata.
  8. The partial order state space reduction. The symmetry state space reduction. An overview of other state space reduction methods. Compositional verification.
  9. Methods of automated abstraction of systems, the predicate abstraction, the counter-example guided abstraction refinement loop, Craig interpolation.
  10. Decision procedures and modern methods of SAT and SMT solving and their use in formal verification (e.g., in the predicate abstraction).
  11. Classical dataflow analyses (such as live variables, available expressions, etc.) as well as some selected, more advanced dataflow analyses (like some pointer analyses), their description via flow equations, and iterative methods of solving these methods.
  12. Abstract interpretation and its use for defining static analyses.
  13. Static analyses based on searching for bug patterns, a note on selected dynamic analyses, esp. those for detecting concurrency-related errors.

Project

13 hod., optionally

Teacher / Lecturer

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