Přístupnostní navigace
E-application
Search Search Close
Course detail
FIT-FADAcad. year: 2023/2024
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
Number of ECTS credits
Mode of study
Guarantor
Department
Entry knowledge
Rules for evaluation and completion of the course
Aims
Study aids
Prerequisites and corequisites
Basic literature
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking, MIT Press, 2000. ISBN 0-262-03270-8
Berard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P., McKenzie, P.: Systems and Software Verification: Model-Checking Techniques and Tools, Springer-Verlag, 2001. ISBN 3-540-41523-8
Monin, J.F., Hinchey, M.G.: Understanding Formal Methods, Springer-Verlag, 2003. ISBN 1-852-33247-6
Valmari, A.: The State Explosion Problem. In Reisig, W., Rozenberg, G.: Lectures on Petri Nets I: Basic Models, Lecture Notes in Computer Science, č.1491, s. 429-528. Springer-Verlag, 1998. ISBN 3-540-65306-6
Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis, Springer-Verlag, 2005. ISBN 3-540-65410-0
Schwartzbach, M.I.: Lecture Notes on Static Analysis, BRICS, Department of Computer Science, University of Aarhus, Denmark, 2006.
Recommended reading
Classification of course in study plans
branch DVI4 , any year of study, winter semester, elective
Lecture
Teacher / Lecturer
Syllabus
Guided consultation in combined form of studies