Program Verification Using Finite Abstraction and Logics

• Thesis title in English: Program Verification Using Finite Abstraction and Logics
• Key words: verification, analysis, logic, abstraction
• Academic year of topic announcement: 2012/2013
• Thesis type: dissertation
• Thesis language: angličtina
• Department: Department of Distributed and Dependable Systems (32-KDSS)
• Supervisor: doc. RNDr. Pavel Parízek, Ph.D.
• Author: hidden - assigned and confirmed by the Study Dept.
• Date of registration: 27.09.2013
• Date of assignment: 27.09.2013
• Confirmed by Study dept. on: 22.01.2014

Guidelines

The goal of this work is to develop new techniques for automated verification of programs that use dynamic data structures, unbounded values of numeric types, and multiple threads.
Such programs are heavily used in critical systems, where errors are very costly. Program verification techniques can detect many subtle errors that are not discovered by traditional testing.
The proposed techniques will be based mainly on finite abstractions of program behavior and logic.

References

1. C. Baier and J.-P. Katoen. Principles of Model Checking. MIT Press 2008
2. D. Kroening and O. Strichman. Decision Procedures: An Algorithmic Point of View. Springer 2008