Name
Abstract | ||
|---|---|---|
Precondition inference is a non-trivial task with several applications in program analysis and verification. We present a novel iterative method for automatically deriving sufficient preconditions for safety and unsafety of programs which introduces a new dimension of modularity. Each iteration maintains over-approximations of the set of emph{safe} and emph{unsafe} emph{initial} states. Then we repeatedly use the current abstractions to partition the programu0027s emph{initial} states into those known to be safe, known to be unsafe and unknown, and construct a revised program focusing on those initial states that are not yet known to be safe or unsafe. An experimental evaluation of the method on a set of software verification benchmarks shows that it can solve problems which are not solvable using previous methods. |
Year | Venue | DocType |
|---|---|---|
2018 | arXiv: Logic in Computer Science | Journal |
Volume | Citations | PageRank |
abs/1811.06771 | 0 | 0.34 |
References | Authors | |
0 | 5 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| bishoksan kafle | 1 | 39 | 7.88 |
| Graeme Gange | 2 | 137 | 24.27 |
| Peter Schachte | 3 | 256 | 22.76 |
| Harald Søndergaard | 4 | 858 | 79.52 |
| Peter J. Stuckey | 5 | 4368 | 457.58 |