Faster FDR Counterexample Generation Using SAT−Solving

With the flourishing development of efficient SAT-solvers, bounded model checking (BMC) has proven to be an extremely powerful symbolic model checking technique. In this paper, we address the problem of applying BMC to concurrent systems involving the interaction of multiple processes running in par...

Full description

Bibliographic Details
Main Authors: Palikareva, H, Ouaknine, J, Roscoe, A
Other Authors: Roggenbach, M
Format: Journal article
Published: 2009