Name
Abstract | ||
|---|---|---|
The construction of a proof for unsatisfiability is less costly than the construction of a ranking function. We present a new approach to LTL software model checking (i.e., to statically analyze a program and verify a temporal property from the full class of LTL including general liveness properties) which aims at exploiting this fact. The idea is to select finite prefixes of a path and check these for infeasibility before considering the full infinite path. We have implemented a tool which demonstrates the practical potential of the approach. In particular, the tool can verify several benchmark programs for a liveness property just with finite prefixes (and thus without the construction of a single ranking function). |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1007/978-3-319-21690-4_4 | COMPUTER AIDED VERIFICATION, PT I |
DocType | Volume | ISSN |
Conference | 9206 | 0302-9743 |
Citations | PageRank | References |
11 | 0.50 | 31 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Daniel Dietsch | 1 | 80 | 13.53 |
| Matthias Heizmann | 2 | 193 | 18.14 |
| Vincent Langenfeld | 3 | 11 | 0.50 |
| Andreas Podelski | 4 | 2760 | 197.87 |