Name
Abstract | ||
|---|---|---|
We propose trace logic, an instance of many-sorted first-order logic, to automate the partial correctness verification of programs containing loops. Trace logic generalizes semantics of program locations and captures loop semantics by encoding properties at arbitrary timepoints and loop iterations. We guide and automate inductive loop reasoning in trace logic by using generic trace lemmas capturing inductive loop invariants. Our work is implemented in the Rapid framework, by extending and integrating superposition-based first-order reasoning within Rapid. We successfully used Rapid to prove correctness of many programs whose functional behavior are best summarized in the first-order theories of linear integer arithmetic, arrays and inductive data types. |
Year | DOI | Venue |
|---|---|---|
2020 | 10.34727/2020/isbn.978-3-85448-042-6_33 | 2020 Formal Methods in Computer Aided Design (FMCAD) |
Keywords | DocType | ISSN |
generic trace lemmas,inductive loop invariants,superposition-based first-order reasoning,trace logic,many-sorted first-order logic,program locations,loop semantics,arbitrary timepoints,loop iterations,automate inductive loop reasoning | Conference | 2641-8177 |
ISBN | Citations | PageRank |
978-1-7281-5633-0 | 0 | 0.34 |
References | Authors | |
10 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Pamina Georgiou | 1 | 1 | 0.70 |
| Bernhard Gleiss | 2 | 2 | 2.07 |
| Laura Kovács | 3 | 494 | 36.97 |