FI:IA159 FM for Software Analysis - Course Information

IA159 Formal Methods for Software Analysis

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

• Image Processing and Analysis (programme FI, N-VIZ)
• Applied Informatics (programme FI, N-AP)
• Information Technology Security (eng.) (programme FI, N-IN)
• Information Technology Security (programme FI, N-IN)
• Bioinformatics and systems biology (programme FI, N-UIZD)
• Bioinformatics (programme FI, N-AP)
• Computer Games Development (programme FI, N-VIZ_A)
• Computer Graphics and Visualisation (programme FI, N-VIZ_A)
• Computer Networks and Communications (programme FI, N-PSKB_A)
• Cybersecurity Management (programme FI, N-RSSS_A)
• Discrete algorithms and models (programme FI, N-TEI)
• Formal analysis of computer systems (programme FI, N-TEI)
• Graphic design (programme FI, N-VIZ)
• Graphic Design (programme FI, N-VIZ_A)
• Hardware Systems (programme FI, N-PSKB_A)
• Hardware systems (programme FI, N-PSKB)
• Image Processing and Analysis (programme FI, N-VIZ_A)
• Information security (programme FI, N-PSKB)
• Information Systems (programme FI, N-IN)
• Information Security (programme FI, N-PSKB_A)
• Quantum and Other Nonclassical Computational Models (programme FI, N-TEI)
• Parallel and Distributed Systems (programme FI, N-IN)
• Computer graphics and visualisation (programme FI, N-VIZ)
• Computer Graphics (programme FI, N-IN)
• Computer Networks and Communication (programme FI, N-IN)
• Computer Networks and Communications (programme FI, N-PSKB)
• Computer Systems (programme FI, N-IN)
• Principles of programming languages (programme FI, N-TEI)
• Embedded Systems (eng.) (programme FI, N-IN)
• Embedded Systems (programme FI, N-IN)
• Cybersecurity management (programme FI, N-RSSS)
• Services development management (programme FI, N-RSSS)
• Software Systems Development Management (programme FI, N-RSSS)
• Services Development Management (programme FI, N-RSSS_A)
• Service Science, Management and Engineering (eng.) (programme FI, N-AP)
• Service Science, Management and Engineering (programme FI, N-AP)
• Social Informatics (programme FI, B-AP)
• Software Systems Development Management (programme FI, N-RSSS_A)
• Software Systems (programme FI, N-PSKB_A)
• Software systems (programme FI, N-PSKB)
• Machine learning and artificial intelligence (programme FI, N-UIZD)
• Theoretical Informatics (programme FI, N-IN)
• Upper Secondary School Teacher Training in Informatics (programme FI, N-SS) (2)
• Artificial Intelligence and Natural Language Processing (programme FI, N-IN)
• Computer Games Development (programme FI, N-VIZ)
• Processing and analysis of large-scale data (programme FI, N-UIZD)
• Image Processing (programme FI, N-AP)
• Natural language processing (programme FI, N-UIZD)

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.

• Enrolment Statistics (Autumn 2023, recent)
  
• Permalink: https://is.muni.cz/course/fi/autumn2023/IA159