Program verification as constraint solving (also for existential and universal CTL properties)

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.

Posted in RiSE Seminar