Přístupnostní navigace
E-application
Search Search Close
Course detail
FIT-FADAcad. year: 2020/2021
An overview of various methods of analysis and verification of programs with formal roots. Model checking: basic principles, specification of properties to be verified, temporal logics, the state explosion problem and existing approaches to solving it, binary decision diagrams, automated abstraction (with a stress on predicate abstraction that plays a key role in software model checking). Various approaches to static analysis: dataflow analysis, pointer analyses, constraint-based analysis, type analysis, abstract interpretation. Deductive verification, SAT solving, SMT solving, symbolic execution. Dynamic analysis with a formal basis, algorithms like FastTrack or dynamic partial order reduction.Areas for the Doctoral State Exam:1. Temporal logics LTL, CTL, and CTL*.2. Büchi automata and LTL model checking based on them.3. CTL model checking.4. Binary decision diagrams.5. Predicate abstraction.6. Abstract interpretation.7. Data-flow analysis.8. SAT solving and SMT solving.9. Symbolic execution.10. Deductive verification.
Language of instruction
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 DVI4 , 0 year of study, winter semester, elective
Lecture
Teacher / Lecturer
Syllabus
Guided consultation in combined form of studies