Course detail

Static Analysis and Verification

FIT-SAVAcad. year: 2022/2023

Introduction of basic terms, such as analysis and verification, formal analysis and verification, soundness and completeness, logical and physical time, safety and liveness, etc. Overview of various approaches to static analysis and verification and other alternative verification approaches. Introduction to temporal logics as one of the classical means of specification of desired system properties. Model checking for the LTL logic using Büchi automata. Use of automatically refined predicate abstraction as one of the most successful approaches towards model checking of software. Abstract interpretation as one of the most successful methods of static analysis: principles, algorithms, and an overview of the most prominent abstract domains. Data flow analysis: basic terms and principles, classical analyses used in optimizing compilers, design of new analyses, pointer analyses. Solving of the SAT and SMT problems, which are used (not only) within a lot of verification approaches. Verification based on symbolic execution, bounded model checking, and k-induction. Deductive verification of annotated programs (functions' pre- and postconditions, loop invariants). Binary decision diagrams as a means of efficient storage of (not only) state spaces. Introduction to automatic verification of termination of program runs (absence of looping) and automatic analysis of complexity.

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 static analysis and verification and with their application within the process of designing computer systems. Students know capabilities and the basic ways of using computer-aided tools for static analysis and verification. Acquired knowledge about the significance and possibilities of using methods and tools of static analysis and verification 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

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

    • Course curriculum

    Not applicable.

    Work placements

    Not applicable.

    Aims

    The goal of the course is to get students acquainted with various methods of static analysis and verification that are commonly used in practice for finding bugs or proving correctness of systems. Students will be introduced to a variety of methods of static analysis and verification with their advantages and disadvantages. Moreover, the course will also present an overview of current tools that implement the discussed techniques and students will, through a project, obtain a first-hand practical experience with a chosen tool.

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

    A project focused at obtaining first-hand practical experience with a selected tool for static analysis or verification and the principles it is based on, reproduction of case studies available for the tool, student's own experiments with the tool, and composition of a report about the tool and the performed experiments.

    Recommended optional programme components

    Not applicable.

    Prerequisites and corequisites

    Not applicable.

    Basic literature

    Not applicable.

    Recommended reading

    Aho, A.V., Lam, S., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison Wesley, 2nd ed., 2006. The part devoted to static analysis.
    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 statickou analýzu a verifikaci.
    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.
    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.

    Elearning

    eLearning: currently opened course

    Classification of course in study plans

    • Programme IT-MSC-2 Master's

      branch MBI , 0 year of study, winter semester, elective
      branch MGM , 0 year of study, winter semester, elective
      branch MMM , 0 year of study, winter semester, compulsory
      branch MPV , 0 year of study, winter semester, elective

    • Programme MITAI Master's

      specialization NADE , 0 year of study, winter semester, elective
      specialization NBIO , 0 year of study, winter semester, elective
      specialization NCPS , 0 year of study, winter semester, elective
      specialization NEMB , 0 year of study, winter semester, elective
      specialization NGRI , 0 year of study, winter semester, elective
      specialization NHPC , 0 year of study, winter semester, elective
      specialization NIDE , 0 year of study, winter semester, elective
      specialization NISD , 0 year of study, winter semester, elective
      specialization NISY up to 2020/21 , 0 year of study, winter semester, elective
      specialization NMAL , 0 year of study, winter semester, elective
      specialization NMAT , 0 year of study, winter semester, compulsory
      specialization NNET , 0 year of study, winter semester, elective
      specialization NSEC , 0 year of study, winter semester, elective
      specialization NSEN , 0 year of study, winter semester, elective
      specialization NSPE , 0 year of study, winter semester, elective
      specialization NVER , 0 year of study, winter semester, compulsory
      specialization NVIZ , 0 year of study, winter semester, elective
      specialization NISY , 0 year of study, winter semester, elective

    • Programme IT-MSC-2 Master's

      branch MBS , 0 year of study, winter semester, compulsory-optional
      branch MIN , 0 year of study, winter semester, compulsory-optional
      branch MIS , 0 year of study, winter semester, compulsory-optional
      branch MSK , 2 year of study, winter semester, compulsory-optional

    • Programme MITAI Master's

      specialization NEMB up to 2021/22 , 0 year of study, winter semester, elective

    Type of course unit

     

    Lecture

    39 hod., optionally

    Teacher / Lecturer

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

    Syllabus

    1. Notion of the terms analysis and verification. Classification of verified properties and systems. Overview of approaches to formal analysis and verification.
    2. Temporal logics CTL*, CTL, and LTL.
    3. Model checking of systems with properties specified in LTL using Büchiho automata.
    4. Model checking using predicate abstraction refined by exclusion of spurious counterexamples.
    5. Abstract Interpretation I: basic notions and principles.
    6. Abstract Interpretation II: an overview of practically successful abstract domains.
    7. Basic notions and principles of data flow analysis, classical data flow analyses.
    8. Advanced data flow analyses, pointer analyses.
    9. Verification of software using symbolic execution.
    10. Deductive verification of annotated programs.
    11. Solutions of the SAT and SMT problems as the enabling technology of many approaches to analysis and verification.
    12. Binary Decision Diagrams.
    13. Verification of termination of programs, automatic analysis of computational complexity.

    Project

    13 hod., compulsory

    Teacher / Lecturer

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

    Syllabus

    First-hand practical experience with a selected tool for static analysis or verification and the principles it is based on, reproduction of case studies available for the tool, student's own experiments with the tool, and composition of a report about the tool and the performed experiments.

    E-learning texts

    T. Vojnar. Static Analysis and Verification: Introduction. 2022/23.
    sav-lecture-01.pdf 0.13 MB

    Elearning

    eLearning: currently opened course