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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Re3ver: Reverse and Verify

  • Adéla Štěpková,
  • Martin Jonáš,
  • Jan Strejček

摘要

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.