Program verification as constraint solving (also for existential and universal CTL properties)
VCLA hosted a RiSE seminar talk by Andrey Rybalchenko on December 13th, 2012.
|DATE:||Thursday, December 13, 2012|
|VENUE:||Seminar room Goedel (Favoritenstrasse 9-11, ground floor, access through courtyard)|
First, we review how proving reachability and termination properties of transition systems, procedural programs, multi-threaded programs, and higher- order functional programs can be reduced to constraint solving. Second, we show how CTL* properties can be proved using contraint-based setting.
Finally, we discuss adequate solving algorithms and tools.