Formal Software Verification

Course Description

Mathematically based specification, development and verification procedures of software systems, aspiring to enhance the quality of final product and at the same time cut down time-to-market period. Temporal logic and its forms. Specification and verification of computational and reactive systems. Formal verification of real programs. Abstraction and symbolic verification principles. Hoare logic and separation logic. Theorem proving and model checking verification algorithms: BDDs, SAT-solvers, SMT-solvers. Tools for automated formal system verification. Application of formal verification in diverse domains of software engineering.

Learning Outcomes

  1. distinguish between correct and incorrect program system behavior
  2. apply formal logic in expressing desired program system behavior
  3. analyze the output of tool for formal verification of software
  4. develop a simple system for program verification by applying some of the verification algorithms
  5. select a suitable algorithm and tool for efficient formal verification of software, depending on the problem
  6. create abstractions of real program systems suitable for verification

Forms of Teaching

Lectures

Live or online

Laboratory

Homeworks

Grading Method

Continuous Assessment Exam
Type Threshold Percent of Grade Threshold Percent of Grade
Homeworks 40 % 40 % 40 % 40 %
Mid Term Exam: Written 0 % 30 % 0 %
Final Exam: Written 0 % 30 %
Exam: Written 33 % 60 %

Week by Week Schedule

  1. Introduction to formal verification of software. Role of formal specification and analysis techniques in the software development cycle. Program assertion languages and analysis approaches. Formal approaches to software modeling and analysis. Tools in support of formal methods. Specification languages, testing languages, and verification languages.
  2. Propositional and predicate logic for formal verification. Syntax and semantics. Formal systems: terminology. Natural deduction.
  3. Temporal CTL logic for reactive software verification. Model checking of reactive software. Automatic and automata based programming for concurrent systems. Communicating processes, fairness checking. NuSMV / NuXMV system.
  4. Temporal logics LTL and CTL* for reactive software verification. Model checking of reactive software. Automatic and automata based programming for concurrent systems.
  5. Formal verification of real programs. Principles of state matching and partial order reduction. State space explosion. Java Pathfinder example.
  6. Hoare logic and separation logic. Application examples.
  7. Preparation for midterm exam
  8. Midterm exam
  9. Boolean functions representation. BDD diagrams. ITE algorithm.
  10. Satisfiability problem. Known SAT solvers. Construction of a SAT solver.
  11. Satisfiability modulo theory (SMT) problem. SMT solvers.
  12. Constraint solvers application in symbolic program execution.
  13. Contemporary challenges in formal verification of programs.
  14. Preparation for final exam.
  15. Final exam

Study Programmes

University graduate
[FER3-HR] Audio Technologies and Electroacoustics - profile
Elective Courses (2. semester)
[FER3-HR] Communication and Space Technologies - profile
Elective Courses (2. semester)
[FER3-HR] Computational Modelling in Engineering - profile
Elective Courses (2. semester)
[FER3-HR] Computer Engineering - profile
Elective Course of the profile (2. semester)
Elective Courses (2. semester)
[FER3-HR] Computer Science - profile
Core-elective courses (2. semester)
[FER3-HR] Control Systems and Robotics - profile
Elective Courses (2. semester)
[FER3-HR] Data Science - profile
Elective Courses (2. semester)
[FER3-HR] Electrical Power Engineering - profile
Elective Courses (2. semester)
[FER3-HR] Electric Machines, Drives and Automation - profile
Elective Courses (2. semester)
[FER3-HR] Electronic and Computer Engineering - profile
Elective Courses (2. semester)
[FER3-HR] Electronics - profile
Elective Courses (2. semester)
[FER3-HR] Information and Communication Engineering - profile
Elective Courses (2. semester)
[FER3-HR] Network Science - profile
Elective Courses (2. semester)
[FER3-HR] Software Engineering and Information Systems - profile
Elective Courses (2. semester)
[FER2-HR] Computer Engineering - profile
Theoretical Course (2. semester)
[FER2-HR] Computer Science - profile
Theoretical Course (2. semester)
[FER2-HR] Information Processing - profile
Theoretical Course (2. semester)
[FER2-HR] Software Engineering and Information Systems - profile
Theoretical Course (2. semester)
[FER2-HR] Telecommunication and Informatics - profile
Theoretical Course (2. semester)

Literature

(.), Mordechai Ben-Ari (2012.), Mathematical Logic for Computer Science, Springer,
(.), Daniel Kroening, Ofer Strichman (2016.), Decision Procedures: An Algorithmic Point of View, 2nd Ed., Springer,
(.), Armin Biere, Marijn Heule, Hans van Maaren, Toby Walsh (2021.), Handbook of Satisfiability, 2nd Ed., IOS Press, 2021.,
(.), Klaus Schneider (2010.), Verification of Reactive Systems: Formal Methods and Algorithms, Springer,
(.), Michael Huth, Mark Ryan (2004.), Logic in Computer Science, Cambridge University Press,
(.), S. Demri, V. Goranko, M. Lange, Temporal Logics in Computer Science: Finite State Systems, Cambridge University Press, 2016.,

Laboratory exercises

For students

General

ID 222519
  Summer semester
5 ECTS
L0 English Level
L1 e-Learning
45 Lectures
0 Seminar
0 Exercises
13 Laboratory exercises
0 Project laboratory

Grading System

88 Excellent
75 Very Good
63 Good
50 Sufficient