Katalin Fazekas,
"EUF-Proofs for SMT4J"
, Johannes Kepler Universität, Linz, 8-2015
Original Titel:
EUF-Proofs for SMT4J
Sprache des Titels:
Englisch
Original Kurzfassung:
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.
Forschungs-