SMT proof checking using a logical framework

DOI10.1007/S10703-012-0163-3MaRDI QIDQ2441776zbMATH OpenOpenAlexFDO

Authors Aaron Stump, Duckki Oe, Andrew Reynolds, Liana Hadarean, Cesare Tinelli

Publication date 28 March 2014

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10703-012-0163-3

zbMATH Keywords

Edinburgh logical frameworkLFSCproof checkingsatisfiability modulo theories

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Semantics in the theory of computing (68Q55) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• Rocket-Fast Proof Checking for SMT Solvers
• Fine grained SMT proofs for the theory of fixed-width bit-vectors
• Efficient, verified checking of propositional proofs
• Computer Aided Verification
• SMTCoq: a plug-in for integrating SMT solvers into Coq

Cites work

• A framework for defining logics
• A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
• Bounded model checking using satisfiability solving
• Deciding Effectively Propositional Logic Using DPLL and Substitution Sets
• Efficiently checking propositional refutations in HOL theorem provers
• Fast LCF-Style Proof Reconstruction for Z3
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
• Ground Interpolation for Combined Theories
• Handbook of automated reasoning. In 2 vols
• scientific article; zbMATH DE number 2090309 (Why is no real title available?)
• scientific article; zbMATH DE number 2090312 (Why is no real title available?)
• scientific article; zbMATH DE number 2090315 (Why is no real title available?)
• scientific article; zbMATH DE number 1392299 (Why is no real title available?)
• Information Security
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Interpolation and SAT-based model checking.
• Isabelle/HOL. A proof assistant for higher-order logic
• Lazy satisfiability modulo theories
• Model Checking Software
• Oracle-based checking of untrusted software
• Rocket-Fast Proof Checking for SMT Solvers
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Towards a mechanized metatheory of Standard ML
• Types for Proofs and Programs

Cited in

(16)

• A semantic framework for proof evidence
• A flexible proof format for SAT solver-elaborator communication
• Reliable reconstruction of fine-grained proofs in a proof assistant
• Flexible proof production in an industrial-strength SMT solver
• A unified framework for DPLL(T) + certificates
• Semi-intelligible Isar proofs from machine-generated proofs
• Modular SMT proofs for fast reflexive checking inside Coq
• Satisfiability modulo theories
• Fine grained SMT proofs for the theory of fixed-width bit-vectors
• scientific article; zbMATH DE number 2090315 (Why is no real title available?)
• Rocket-Fast Proof Checking for SMT Solvers
• Scalable fine-grained proofs for formula processing
• Scalable fine-grained proofs for formula processing
• \textsc{Carcara}: an efficient proof checker and elaborator for SMT proofs in the Alethe format
• Improving the SMT proof reconstruction pipeline in Isabelle/HOL
• CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver

Describes a project that uses

Uses Software

• cvc3
• veriT
• SMT-LIB
• ESC/Java
• Coq
• Why3
• z3
• Boogie
• CLSAT
• seL4

This page was built for publication: SMT proof checking using a logical framework

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2441776)