Pages that link to "Item:Q5899057"
From MaRDI portal
The following pages link to Tools and Algorithms for the Construction and Analysis of Systems (Q5899057):
Displaying 24 items.
- Combining decision procedures by (model-)equality propagation (Q436376) (← links)
- Resolution proof transformation for compression and interpolation (Q479815) (← links)
- Translating FSP into LOTOS and networks of automata (Q613134) (← links)
- Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs (Q832719) (← links)
- Efficiently checking propositional refutations in HOL theorem provers (Q1006729) (← links)
- Data compression for proof replay (Q1040776) (← links)
- Combination of convex theories: modularity, deduction completeness, and explanation (Q1041593) (← links)
- A semantic framework for proof evidence (Q1701039) (← links)
- Flexible proof production in an industrial-strength SMT solver (Q2104495) (← links)
- Extending Sledgehammer with SMT solvers (Q2351158) (← links)
- A unified framework for DPLL(T) + certificates (Q2375732) (← links)
- SMT proof checking using a logical framework (Q2441776) (← links)
- Verification of clock synchronization algorithms: experiments on a combination of deductive tools (Q2642981) (← links)
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler (Q2655335) (← links)
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses (Q3100209) (← links)
- Modular SMT Proofs for Fast Reflexive Checking Inside Coq (Q3100210) (← links)
- Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL (Q3100212) (← links)
- Satisfiability Modulo Theories (Q3176369) (← links)
- LCF-Style Propositional Simplification with BDDs and SAT Solvers (Q3543649) (← links)
- Compressing Propositional Refutations (Q5178991) (← links)
- Extending Sledgehammer with SMT Solvers (Q5200019) (← links)
- Rocket-Fast Proof Checking for SMT Solvers (Q5458346) (← links)
- Bounded Relational Analysis of Free Data Types (Q5458813) (← links)
- Scalable fine-grained proofs for formula processing (Q5919479) (← links)
