Publication details
Re3ver: Reverse and Verify
| Authors | |
|---|---|
| Year of publication | 2026 |
| Type | Paper in proceedings |
| Conference | Tools and Algorithms for the Construction and Analysis of Systems - 32nd International Conference, TACAS 2026, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2026, Turin, Italy, April 11-16, 2026, Proceedings, Part II |
| MU Faculty or unit | |
| Citation | |
| web | https://link.springer.com/chapter/10.1007/978-3-032-22749-2_32 |
| Doi | https://doi.org/10.1007/978-3-032-22749-2_32 |
| Keywords | software verification; program reversal; SV-COMP |
| Description | Most verifiers analyze a given program in a forward manner, i.e., along its control flow. However, there are many programs where the reason for the unreachability of error locations is near these locations. To efficiently verify these programs with forward verification algorithms, we designed and implemented a technique that reverses the given program before its verification. This paper describes a new experimental tool Re3ver, which combines the program reversal and the established verifier Symbiotic based on program slicing and symbolic execution. |
| Related projects: |