Formalizing Complex Specifications for Software Model Checking
Separating property definitions from source code using specification automata
This talk focuses on the formal representation of complex properties in software model checking, independent of the analyzed source code.
Instead of instrumenting the program, properties are expressed as specification automata and checked directly against the original code. The presentation reviews existing approaches in this area, identifies remaining open challenges, and demonstrates the practical benefits of separating specifications from implementation.
Such a separation enables more reusable, scalable, and maintainable verification workflows, and is particularly important for verifying large, real-world software systems.