Martin Suda

Date: 17:00, Tuesday, January 12, 2016
Speaker: Martin Suda
Venue: TU Wien
Notes:

Day: Tuesday,             Room: Menger

In this talk I will give an overview of my PhD work, in which I explored the potential of resolution-based methods for linear temporal reasoning. On the abstract level, this means the development of new algorithms for automated reasoning about properties of systems which evolve in time. More concretely, I will: 1) show how to adapt the superposition framework to proving theorems in propositional Linear Temporal Logic (LTL), 2) use a connection between superposition and the CDCL calculus of modern SAT solvers to come up with an efficient LTL prover, 3) specialize the previous to reachability properties and discover a close connection to Property Directed Reachability (PDR), an algorithm recently developed for model checking of hardware circuits, 4) further improve PDR by providing a new technique for enhancing clause propagation phase of the algorithm, and 5) adapt PDR to automated planning by replacing the SAT solver inside with a planning-specific procedure.

 

Posted in RiSE Seminar