Hier finden Sie wissenschaftliche Publikationen aus den Fraunhofer-Instituten.

Proof logging for computer algebra based SMT solving

: Marx, O.; Wedler, M.; Stoffel, D.; Kunz, W.; Dreyer, A.


Institute of Electrical and Electronics Engineers -IEEE-; Institute of Electrical and Electronics Engineers -IEEE-, Council on Electronic Design Automation; Association for Computing Machinery -ACM-; Association for Computing Machinery -ACM-, Special Interest Group on Design Automation -SIGDA-:
IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2013 : San Jose, California, USA, 18 - 21 November 2013
Piscataway, NJ: IEEE, 2013
ISBN: 978-1-4799-1070-0
ISBN: 978-1-4799-1071-7
International Conference on Computer-Aided Design (ICCAD) <2013, San Jose/Calif.>
Conference Paper
Fraunhofer ITWM ()

In formal verification, proof logging is a technique for automatically reviewing the reasoning steps of a proof engine by a separate tool. This is useful for enhancing the confidence in the prover's result, especially in the case of a positive answer when no counterexample exists. Mature proof logging techniques exist for single-theory provers. SMT solvers, however, combine several theories so that developing an unified proof logging technique is more challenging. This paper proposes an approach for logging the proofs of the SMT solver STABLE which is a prover combining SAT and computer algebra engines. We show how to translate the SAT proofs into algebraic forms (polynomials) and how to check the combined Boolean and word-level proofs using a separate computer algebra engine.