Přístupnostní navigace
E-application
Search Search Close
Course detail
FIT-SAVAcad. year: 2020/2021
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
Learning outcomes of the course unit
Prerequisites
Co-requisites
Planned learning activities and teaching methods
Assesment methods and criteria linked to learning outcomes
Course curriculum
Work placements
Aims
Specification of controlled education, way of implementation and compensation for absences
Recommended optional programme components
Prerequisites and corequisites
Basic literature
Recommended reading
Classification of course in study plans
branch MBI , any year of study, winter semester, electivebranch MPV , any year of study, winter semester, electivebranch MGM , any year of study, winter semester, electivebranch MIS , any year of study, winter semester, compulsory-optionalbranch MBS , any year of study, winter semester, compulsory-optionalbranch MIN , any year of study, winter semester, compulsory-optionalbranch MMI , any year of study, winter semester, electivebranch MMM , any year of study, winter semester, compulsory
specialization NADE , any year of study, winter semester, electivespecialization NBIO , any year of study, winter semester, electivespecialization NGRI , any year of study, winter semester, electivespecialization NNET , any year of study, winter semester, electivespecialization NVIZ , any year of study, winter semester, electivespecialization NCPS , any year of study, winter semester, electivespecialization NSEC , any year of study, winter semester, electivespecialization NEMB , any year of study, winter semester, electivespecialization NHPC , any year of study, winter semester, electivespecialization NISD , any year of study, winter semester, electivespecialization NIDE , any year of study, winter semester, electivespecialization NISY , any year of study, winter semester, electivespecialization NMAL , any year of study, winter semester, electivespecialization NMAT , any year of study, winter semester, compulsoryspecialization NSEN , any year of study, winter semester, electivespecialization NVER , any year of study, winter semester, compulsoryspecialization NSPE , any year of study, winter semester, elective
branch MSK , 2. year of study, winter semester, compulsory-optional
Lecture
Teacher / Lecturer
Syllabus
Project
E-learning texts