Přístupnostní navigace
E-application
Search Search Close
Course detail
FIT-SAVAcad. year: 2024/2025
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
Number of ECTS credits
Mode of study
Guarantor
Department
Entry knowledge
Rules for evaluation and completion of the course
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.
Aims
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.
Study aids
Prerequisites and corequisites
Basic literature
Recommended literature
Classification of course in study plans
specialization NGRI , 0 year of study, winter semester, electivespecialization NADE , 0 year of study, winter semester, electivespecialization NISD , 0 year of study, winter semester, electivespecialization NMAT , 0 year of study, winter semester, compulsoryspecialization NSEC , 0 year of study, winter semester, electivespecialization NISY up to 2020/21 , 0 year of study, winter semester, electivespecialization NNET , 0 year of study, winter semester, electivespecialization NMAL , 0 year of study, winter semester, electivespecialization NCPS , 0 year of study, winter semester, electivespecialization NHPC , 0 year of study, winter semester, electivespecialization NVER , 0 year of study, winter semester, compulsoryspecialization NIDE , 0 year of study, winter semester, electivespecialization NISY , 0 year of study, winter semester, electivespecialization NEMB , 0 year of study, winter semester, electivespecialization NSPE , 0 year of study, winter semester, electivespecialization NEMB , 0 year of study, winter semester, electivespecialization NBIO , 0 year of study, winter semester, electivespecialization NSEN , 0 year of study, winter semester, electivespecialization NVIZ , 0 year of study, winter semester, elective
Lecture
Teacher / Lecturer
Syllabus
Project
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