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
Bibliographic Details
- Journal:
- Electronic Communications of the EASST
- Volume:
- 23
- Publication date:
- 2009-09-01
Item Description
- UUID:
-
uuid:0b117810-5a97-4c82-a38e-caae1ab6b419
- Local pid:
- cs:3297
- Deposit date:
- 2015-03-31
Terms of use
- Copyright date:
- 2009
If you are the owner of this record, you can report an update to it here: Report update to this record