Andrey Rybalchenko

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.

Comments are closed.