Name
Abstract | ||
|---|---|---|
We extended ESBMC to exploit the combination of context-bounded symbolic model checking and k-induction to prove safety properties in single- and multi-threaded ANSI-C programs with unbounded loops. We now first try to verify by induction that the safety property holds in the system. If that fails, we search for a bounded reachable state that constitutes a counterexample. |
Year | Venue | Field |
|---|---|---|
2013 | Lecture Notes in Computer Science | Software engineering,Computer science,Theoretical computer science,Management science |
DocType | Volume | ISSN |
Conference | 7795 | 0302-9743 |
Citations | PageRank | References |
5 | 0.41 | 5 |
Authors | ||
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 | 206 | 15.53 |