Combining Symbolic Execution with Predicate Abstraction and CEGAR
| Authors | |
|---|---|
| Year of publication | 2024 |
| Type | Article in Proceedings |
| Conference | Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 |
| MU Faculty or unit | |
| Citation | |
| web | https://repositum.tuwien.at/handle/20.500.12708/200800 |
| Doi | http://dx.doi.org/10.34727/2024/isbn.978-3-85448-065-5_33 |
| Keywords | program verification; symbolic execution; predicate abstraction; CEGAR |
| Description | The paper presents a simple, yet effective program verification technique that combines symbolic execution with implicit predicate abstraction and CEGAR. The technique can prove correctness of many programs that are beyond the reach of the standard symbolic execution because their symbolic execution tree is prohibitively large or even infinite. The technique has been implemented in the software model checker KRATOS. Our experimental evaluation shows that it also decides correctness of some programs that were decided neither by the standard symbolic execution nor by IC3 with predicate abstraction (all implemented in KRATOS). |
| Related projects: |