SMT proof checking using a logical framework
From MaRDI portal
Recommendations
Cites work
- 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?)
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- A framework for defining logics
- 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
- 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
(15)- Flexible proof production in an industrial-strength SMT solver
- CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver
- Scalable fine-grained proofs for formula processing
- Semi-intelligible Isar proofs from machine-generated proofs
- Fine grained SMT proofs for the theory of fixed-width bit-vectors
- Reliable reconstruction of fine-grained proofs in a proof assistant
- Rocket-Fast Proof Checking for SMT Solvers
- A unified framework for DPLL(T) + certificates
- A flexible proof format for SAT solver-elaborator communication
- Modular SMT proofs for fast reflexive checking inside Coq
- scientific article; zbMATH DE number 2090315 (Why is no real title available?)
- Satisfiability modulo theories
- Scalable fine-grained proofs for formula processing
- A semantic framework for proof evidence
- \textsc{Carcara}: an efficient proof checker and elaborator for SMT proofs in the Alethe format
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)
