EUF-Proofs for SMT4J

SMT (Satisfiability Modulo Theories) Solvers are considered as a new, promising generation of decision engines in numerous software and hardware verification tools due to their support of various decision procedures for theories beyond propositional logic. One general theory that is supported by most SMT Solvers is specialized in equalities over uninterpreted functions (EUF). In this theory one can decide whether an equality is a logical consequence (in first-order logic with equality) of a conjunction of equalities. Since SMT Solvers are fairly complex systems with a large, frequently growing code base, the objective to ensure their correctness is highly challenging. Therefore unsatisfiable core production i.e., the extraction of an unsatisfiable subformula which is as small as possible, and detailed proof generation on the level of theories are desirable functions of an SMT Solver. The constructed unsatisfiable cores can be exploited to build stronger theory lemmas which reduce the search space considerably. The generated proofs can be verified automatically by external tools to achieve higher level of confidence about the correctness of the solver. SMT4J (SMT for Java) is a simple, java-based lazy SMT Solver that neither supported the generation of proofs nor exploited the power of unsatisfiable cores for pruning the search space. The main contribution of this thesis is the extension of the EUF theory solver of SMT4J with unsatisfiable core generation capability based on a congruence closure algorithm. Furthermore, this work extends the theory solver with detailed proof production functionality in order to ensure the quality of the produced results. In extensive experiments considerable run time improvements can be observed if the unsatisfiable cores are used. Furthermore, it is shown that proof generation can be efficiently integrated into the solving process.