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. Mathematical logic as a foundation for specification languages. Temporal logic and its forms. Specification and verification of computational and reactive systems. Abstraction and symbolic verification principles. 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. 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.
  3. Temporal logics LTL and CTL* for reactive software verification. Model checking of reactive software. Automatic and automata based programming for concurrent systems.
  4. Formal verification of real programs. Principles of state matching and partial order reduction. State space explosion. Java Pathfinder example.
  5. Abstract interpretation and predicate abstraction. Program abstraction, refining abstraction, CEGAR method.
  6. Hoare logic and separation logic. Application examples.
  7. Preparation for midterm exam
  8. Midterm exam
  9. Satisfiability problem. Known SAT-solvers. Construction of a SAT solver.
  10. Boolean functions representation. BDD diagrams. ITE algorithm.
  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
Audio Technologies and Electroacoustics (profile)
Free Elective Courses (2. semester)
Communication and Space Technologies (profile)
Free Elective Courses (2. semester)
Computational Modelling in Engineering (profile)
Free Elective Courses (2. semester)
Computer Engineering (profile)
Elective Course of the profile (2. semester)
Computer Science (profile)
Core-elective courses (2. semester)
Control Systems and Robotics (profile)
Free Elective Courses (2. semester)
Data Science (profile)
Free Elective Courses (2. semester)
Electrical Power Engineering (profile)
Free Elective Courses (2. semester)
Electric Machines, Drives and Automation (profile)
Free Elective Courses (2. semester)
Electronic and Computer Engineering (profile)
Free Elective Courses (2. semester)
Electronics (profile)
Free Elective Courses (2. semester)
Information and Communication Engineering (profile)
Free Elective Courses (2. semester)
Network Science (profile)
Free Elective Courses (2. semester)
Software Engineering and Information Systems (profile)
Free Elective Courses (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,
(.), Christel Baier, Joost Pieter Katoen (2008.), Principles of Model Checking, MIT Press,
(.), 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.,

For students

General

ID 222519
  Summer semester
5 ECTS
L0 English Level
L1 e-Learning
45 Lectures
13 Laboratory exercises

Grading System

88 Excellent
75 Very Good
63 Good
50 Acceptable