The \textsc{Golem} Horn solver

DOI10.1007/978-3-031-37703-7_10MaRDI QIDQ6535535zbMATH OpenFDO

Authors Martin Blicha, Konstantin Britikov, Natasha Sharygina

Publication date 12 January 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-37703-7_10

zbMATH Keywords

model checkingconstrained Horn clauses

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Horn clause solvers for program verification
• Solving constrained Horn clauses over algebraic data types
• Probabilistic Horn clause verification
• Solving Horn clauses on inductive data types without induction

Cites work

• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 7444022 (Why is no real title available?)
• scientific article; zbMATH DE number 7453201 (Why is no real title available?)
• scientific article; zbMATH DE number 7806143 (Why is no real title available?)
• A unifying view on SMT-based software verification
• Accelerating interpolants
• Generalized property directed reachability
• Global guidance for local generalization in model checking
• Guiding Craig interpolation with domain-specific abstractions
• HoIce: an ICE-based non-linear Horn clause solver
• Horn clauses for communicating timed systems
• ICE-based refinement type discovery for higher-order functional programs
• Interpolation and SAT-based model checking.
• Lazy Abstraction with Interpolants
• Learning inductive invariants by sampling from frequency distributions
• Maximizing branch coverage with constrained Horn clauses
• OpenSMT2: an SMT solver for multi-core and cloud computing
• PeRIPLO: a framework for producing effective interpolants in SAT-based software verification
• RustHorn: CHC-based verification for Rust programs
• SAT-Based Model Checking without Unrolling
• SMT-based model checking for recursive programs
• Software verification with PDR: an implementation of the state of the art
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
• Transition power abstractions for deep counterexample detection
• Tree automata-based refinement with application to Horn clause verification

Cited in

(3)

• Infinite state model checking by learning transitive relations
• \textsc{Golem}: a flexible and efficient solver for constrained Horn clauses
• Maximizing branch coverage with constrained Horn clauses

This page was built for publication: The \textsc{Golem} Horn solver

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