Journal article icon

Journal article

Faster FDR Counterexample Generation Using SAT−Solving

Abstract:

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 parallel. We adapt the BMC framework to the context of CSP and FDR yielding bounded refinement checking. Refinement checking reduces to checking for reverse containment of possible behaviours. Therefo...

Expand abstract

Actions


Access Document


Files:

Authors


Hristina Palikareva More by this author
Joel Ouaknine More by this author
A.W. Roscoe More by this author

Contributors

Journal:
Electronic Communications of the EASST
Volume:
23
Publication date:
2009-09-01
URN:
uuid:0b117810-5a97-4c82-a38e-caae1ab6b419
Local pid:
cs:3297

Terms of use


Metrics



If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP