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


Contributors

Role:
Editor
Journal:
Electronic Communications of the EASST
Volume:
23
Publication date:
2009-09-01
UUID:
uuid:0b117810-5a97-4c82-a38e-caae1ab6b419
Local pid:
cs:3297
Deposit date:
2015-03-31

Terms of use


Views and Downloads






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

TO TOP