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 |
| TIME: | 14:00 |
| VENUE: | Seminar room Goedel (Favoritenstrasse 9-11, ground floor, access through courtyard) |
ABSTRACT
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.
