Re3ver: Reverse and Verify
摘要
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.