Name
Abstract | ||
|---|---|---|
Checking safety properties is mandatory in the validation process of critical software. When formal verification tools fail to prove some properties, the automatic generation of counterexamples for a given loop depth is achievable, and is therefore an important issue in practice. We propose in this paper a dynamic constraint based exploration strategy for software bounded model checking. Constraint solving is integrated with state exploration to prune state space. Experiments on a real industrial Flasher Manager controller show that our system outperforms state of the art bounded model checking tools. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1145/1982185.1982528 | SAC |
Keywords | Field | DocType |
dynamic constraint,software bounded model checking,art bounded model checking,controller show,critical software,state space,automatic generation,checking safety property,exploration strategy,state exploration,dynamic constraint-based bmc strategy,constraint programming,counterexamples,formal verification | Mathematical optimization,Control theory,Model checking,Computer science,Constraint programming,Software,Constraint logic programming,State space,Bounded function,Formal verification | Conference |
Citations | PageRank | References |
2 | 0.39 | 17 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Hélène Collavizza | 1 | 146 | 13.12 |
| Nguyen Le Vinh | 2 | 3 | 0.74 |
| Michel Rueher | 3 | 613 | 59.81 |
| Samuel Devulder | 4 | 10 | 1.59 |
| Thierry Gueguen | 5 | 2 | 0.39 |