Přístupnostní navigace
E-application
Search Search Close
Course detail
FIT-FADAcad. year: 2024/2025
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
Entry knowledge
Rules for evaluation and completion of the course
Aims
Study aids
Prerequisites and corequisites
Basic literature
Recommended literature
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