Tools and Algorithms for the Construction and Analysis of Systems

DOI10.1007/11691372zbMath1180.68240OpenAlexW2739785336MaRDI QIDQ5899057

Stephan Merz, Alwen Tiu, Jean-Yves Marion, Pascal Fontaine, Leonor Prensa Nieto

Publication date: 2 May 2007

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/11691372

Mathematics Subject Classification ID

Related Items

Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs, A unified framework for DPLL(T) + certificates, Satisfiability Modulo Theories, Verification of clock synchronization algorithms: experiments on a combination of deductive tools, HOL-Boogie -- an interactive prover-backend for the verifying C compiler, Translating FSP into LOTOS and networks of automata, A semantic framework for proof evidence, Combining decision procedures by (model-)equality propagation, SMT proof checking using a logical framework, LCF-Style Propositional Simplification with BDDs and SAT Solvers, Resolution proof transformation for compression and interpolation, Compressing Propositional Refutations, Extending Sledgehammer with SMT Solvers, Rocket-Fast Proof Checking for SMT Solvers, Bounded Relational Analysis of Free Data Types, Efficiently checking propositional refutations in HOL theorem provers, Scalable fine-grained proofs for formula processing, A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses, Modular SMT Proofs for Fast Reflexive Checking Inside Coq, Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL, Data compression for proof replay, Combination of convex theories: modularity, deduction completeness, and explanation, Flexible proof production in an industrial-strength SMT solver, Extending Sledgehammer with SMT solvers

Uses Software

• Isabelle/HOL
• Gandalf