Combining Symbolic Execution with Predicate Abstraction and CEGAR
| Autoři | |
|---|---|
| Rok publikování | 2024 |
| Druh | Článek ve sborníku |
| Konference | Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 |
| Fakulta / Pracoviště MU | |
| Citace | |
| www | https://repositum.tuwien.at/handle/20.500.12708/200800 |
| Doi | http://dx.doi.org/10.34727/2024/isbn.978-3-85448-065-5_33 |
| Klíčová slova | program verification; symbolic execution; predicate abstraction; CEGAR |
| Popis | 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). |
| Související projekty: |