Regular Model Checking Using SAT and SMT Solvers

Speaker

Daniel Neider (I7)

Title Regular Model Checking Using SAT and SMT Solvers
When 22.02.2012, 10:00
Where Room 5052
Abstract We consider regular model checking (of safety properties) and present a novel approach to prove a program correct. Instead of manipulating the input on an automaton-level, we reformulate the problem in terms of logical formulae. We offer implementations in two different logics that can be solved by a SAT or SMT solver, respectively.
Slides