Sireum/Topi LDP: a lightweight semi-decision procedure for optimizing symbolic execution-based analyses

Abstract

Automated theorem proving techniques such as Satisfiability Modulo Theory (SMT) solvers have seen significant advances in the past several years. These advancements, coupled with vast hardware improvements, have drastic impact on, for example, program verification techniques and tools. The general availability of robust general purpose solvers have reduced a significant engineering overhead when designing and developing program verifiers. However, most solver implementations are designed to be used as a black box, and due to their aim as general purpose solvers, they often miss optimization opportunities that can be done by leveraging domain-specific knowledge.