ITMO University
“Programming Technologies” Department

Automata program verifier

Saint-Petersburg State University of Information Technologies, Mechanics and Optics

Bachelor work
Executable code
Executable file
Presentation

Annotation

The project purpose is to verify automata programs model provided by instrumental tool UniMod. This tool generates XML-file and verifier constructs model for verification using only this file. Requirements are written using Linear Time Logic (LTL).

Main verifier's feature is specialization on automata programs model. So model transformation is unnecessary and verifier checks claims about automata program directly. Concurrent double DFS algorithm was implemented in this work, thus verifier was optimized to execute on multi-core systems.