Title:

Static Analysis and Verification

Code:SAV
Ac.Year:2019/2020
Sem:Winter
Curriculums:
ProgrammeField/
Specialization
YearDuty
IT-MSC-2MBI-Compulsory
IT-MSC-2MBS-Compulsory-Elective - group B
IT-MSC-2MGM-Elective
IT-MSC-2MIN-Compulsory-Elective - group B
IT-MSC-2MIS-Compulsory-Elective - group F
IT-MSC-2MMI-Elective
IT-MSC-2MMM-Compulsory
IT-MSC-2MPV-Elective
IT-MSC-2MSK2ndCompulsory-Elective - group M
MITAINADE-Elective
MITAINBIO-Elective
MITAINCPS-Elective
MITAINEMB-Elective
MITAINGRI-Elective
MITAINHPC-Elective
MITAINIDE-Elective
MITAINISD-Elective
MITAINISY-Elective
MITAINMAL-Elective
MITAINMAT-Compulsory
MITAINNET-Elective
MITAINSEC-Elective
MITAINSEN-Elective
MITAINSPE-Elective
MITAINVER-Compulsory
MITAINVIZ-Elective
Language of Instruction:Czech
Credits:5
Completion:credit+exam
Type of
instruction:
Hour/semLecturesSeminar
Exercises
Laboratory
Exercises
Computer
Exercises
Other
Hours:3900013
 ExamsTestsExercisesLaboratoriesOther
Points:6000040
Guarantor:Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
Deputy guarantor:Lengál Ondřej, Ing., Ph.D. (DITS)
Lecturer:Lengál Ondřej, Ing., Ph.D. (DITS)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
Faculty:Faculty of Information Technology BUT
Department:Department of Intelligent Systems FIT BUT
Schedule:
DayLessonWeekRoomStartEndLect.Gr.Groups
TuelecturelecturesE104 18:0020:501MIT 2MIT xx
 
Learning objectives:
  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.
Description:
  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). Introduction to automatic verification of termination of program runs (absence of looping) and automatic analysis of complexity. Static analysis based on error patterns.
Knowledge and skills required for the course:
  Knowledge of discrete mathematics, the theory of formal languages, and algorithmics on the bachelor's level is assumed.
Subject specific learning outcomes and competencies:
  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.
Generic learning outcomes and competencies:
  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.
Why is the course taught:
  The course will introduce students to methods and tools of static analysis and verification, which are growing in use for assuring quality of computer systems. The knowledge of these methods is beneficial for designers of software, as well as hardware, and is of high importance especially for a work within the area of quality assurance. 
Syllabus of lectures:
 
  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. Solutions of the SAT and SMT problems as the enabling technology of many approaches to analysis and verification.
  10. Verification of software using symbolic execution.
  11. Deductive verification of annotated programs.
  12. Verification of termination of programs, automatic analysis of computational complexity.
  13. Static analysis based on matching error patterns. 
Syllabus - others, projects and individual work of students:
 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.
Fundamental literature:
 
  • Clarke, E.M., Henzinger, Th.A., Veith, H., Bloem, R. (Eds.): Handbook of Model Checking, Springer International Publishing, 2018.
  • Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, 2008.
  • 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. 
  • 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.
Study literature:
 
  • Clarke, E.M., Henzinger, Th.A., Veith, H., Bloem, R. (Eds.): Handbook of Model Checking, Springer International Publishing, 2018.
  • 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. 
  • Moller, A., Schwartzbach, M.I.: Static Program Analysis, Department of Computer Science, Aarhus University, Denmark, 2018.
  • 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. 
  • 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. 
  • Materials presented within the lectures and made accessible via the Internet. 
  • Materials freely accessible on the Internet, especially papers and documentation related to the various computer-aided tools for static analysis and verification.
Progress assessment:
  
  • 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.
Exam prerequisites:
  Having at least 50% of the possible point evaluation of the project.
 

Your IPv4 address: 54.198.246.164