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

Automated theorem proving techniques such as Satisfiabil-ity Modulo Theory (SMT) solvers have seen significant ad-vances in the past several years. These advancements, cou-pled 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 de-signing and developing program verifiers. However, most solver implementations are designed to be used as a black box, and due to their aim as as general purpose solvers, they often miss optimization opportunities that can be done by leveraging domain-specific knowledge. This paper presents our effort to leverage domain-specific knowledge for optimizing symbolic execution (SymExe)-based analysis; we present optimization techniques incorporated as a lightweight semi-decision procedure (LDP) that provides up to an order of magnitude faster analysis time when ana-lyzing realistic programs and well-known algorithms. LDP sits in the middle between a SymExe-based analysis tool and an existing SMT solver; it aims to reduce the number of solver calls by intercepting them and attempting to solve constraints using its lightweight deductive engine.