IA159 Formal Methods for Software Analysis

Faculty of Informatics
Autumn 2023
Extent and Intensity
2/0/0. 2 credit(s) (plus extra credits for completion). Type of Completion: zk (examination).
Teacher(s)
prof. RNDr. Jan Strejček, Ph.D. (lecturer)
Guaranteed by
prof. RNDr. Jan Strejček, Ph.D.
Department of Computer Science – Faculty of Informatics
Supplier department: Department of Computer Science – Faculty of Informatics
Timetable
Thu 12:00–13:50 A319
Prerequisites
Some degree of abstract math reasoning.
Course Enrolment Limitations
The course is also offered to the students of the fields other than those the course is directly associated with.
fields of study / plans the course is directly associated with
there are 49 fields of study the course is directly associated with, display
Course objectives
At the end of this course, students should understand and be able to explain principles and applications of basic and selected advanced formal methods for software analysis. Students should be also able to make reasoned decisions about suitability of various methods for given goals and to apply suitable formal methods or tools.
Learning outcomes
At the end of this course, students should understand and be able to explain principles and applications of basic and selected advanced formal methods for software analysis. Students should be also able to make reasoned decisions about suitability of various methods for given goals and to apply suitable formal methods or tools.
Syllabus
  • Formal aspects of testing (coverage criteria, software quality metrics).
  • Automated test generation: greybox fuzzing.
  • Deductive verification.
  • Static analysis and abstract interpretation.
  • Points-to analysis, control and data dependencies, program slicing.
  • Shape analysis.
  • Symbolic execution and bounded model checking, concolic execution, whitebox fuzz testing.
  • Configurable program analysis.
  • Verification via automata, symbolic execution, and Interpolation.
  • Verification witnesses.
Literature
  • PELED, Doron A. Software reliability methods. New York: Springer, 2001, xix, 331. ISBN 0387951067. info
  • CLARKE, E. M., Orna GRUMBERG, Doron PELED, Daniel KROENING and Helmut VEITH. Model checking. Second edition. Cambridge, Massachusetts: MIT Press, 2018, xx, 402. ISBN 9780262038836. info
  • Handbook of model checking. Edited by E. M. Clarke - T. A. Henzinger - Helmut Veith - Roderick Bloem. Cham: Springer International Publishing AG, 2018, xxiv, 1210. ISBN 9783319105741. info
Teaching methods
lectures
Assessment methods
oral exam
Language of instruction
English
Further Comments
Study Materials
The course is taught annually.
The course is also listed under the following terms Spring 2008, Spring 2009, Spring 2010, Spring 2011, Spring 2012, Spring 2013, Spring 2014, Spring 2015, Spring 2016, Spring 2017, Spring 2018, Spring 2019, Spring 2020, Spring 2021, Spring 2022, Spring 2023, Autumn 2024.
  • Enrolment Statistics (Autumn 2023, recent)
  • Permalink: https://is.muni.cz/course/fi/autumn2023/IA159