Publica
Hier finden Sie wissenschaftliche Publikationen aus den FraunhoferInstituten. Proof logging for computer algebra based SMT solving
 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 ComputerAided Design, ICCAD 2013 : San Jose, California, USA, 18  21 November 2013 Piscataway, NJ: IEEE, 2013 ISBN: 9781479910700 ISBN: 9781479910717 pp.677684 
 International Conference on ComputerAided Design (ICCAD) <2013, San Jose/Calif.> 

 English 
 Conference Paper 
 Fraunhofer ITWM () 
Abstract
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 singletheory 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 wordlevel proofs using a separate computer algebra engine.