Sciweavers

MEMOCODE
2003
IEEE

Methods for exploiting SAT solvers in unbounded model checking

14 years 22 days ago
Methods for exploiting SAT solvers in unbounded model checking
— Modern SAT solvers have proved highly successful in finding counterexamples to temporal properties of systems, using a method known as ”bounded model checking”. It is natural to ask whether these solvers can also be exploited for proving correctness. In fact, techniques do exist for proving properties using SAT solvers, but for the most part existing methods are either incomplete or have a low capacity relative to bounded model checking. Here we consider two new methods that exploit a SAT solver’s ability to generate refutations in order to prove properties in an unbounded sense.
Kenneth L. McMillan
Added 05 Jul 2010
Updated 05 Jul 2010
Type Conference
Year 2003
Where MEMOCODE
Authors Kenneth L. McMillan
Comments (0)