Name
Abstract | ||
|---|---|---|
Context-bounded model checking has successfully been used to verify safety properties in multi-threaded systems automatically, even if they are implemented in low-level programming languages like ANSIC. In this paper, we describe and experiment with an approach to extend context-bounded model checking to liveness properties expressed in linear-time temporal logic (LTL). Our approach converts the LTL formulae into Büchi-automata and then further into C monitor threads, which are interleaved with the execution of the program under test. This combined system is then checked using the ESBMC model checker. Since this approach explores a larger number of interleavings than normal context-bounded model checking, we use a state hashing technique which substantially reduces the number of redundant interleavings that are explored and so mitigates state space explosion. Our experimental results show that we can verify non-trivial properties in the firmware of a medical device. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1007/978-3-642-24690-6_21 | SEFM |
Keywords | Field | DocType |
ansi-c software,mitigates state space explosion,context-bounded model checking,normal context-bounded model checking,esbmc model checker,combined system,ltl property,c monitor thread,larger number,ltl formula,redundant interleavings | Abstraction model checking,Model checking,Programming language,ANSI C,Computer science,Real-time computing,Thread (computing),Partial order reduction,Temporal logic,State space,Liveness | Conference |
Volume | ISSN | Citations |
7041 | 0302-9743 | 7 |
PageRank | References | Authors |
0.54 | 20 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jeremy Morse | 1 | 80 | 7.10 |
| Lucas Cordeiro | 2 | 360 | 38.38 |
| Denis Nicole | 3 | 41 | 2.96 |
| Bernd Fischer | 4 | 371 | 28.86 |