The \textsc{Golem} Horn solver
From MaRDI portal
Publication:6535535
DOI10.1007/978-3-031-37703-7_10zbMATH Open1545.68134MaRDI QIDQ6535535FDOQ6535535
Authors: Martin Blicha, Konstantin Britikov, Natasha Sharygina 
Publication date: 12 January 2024
Recommendations
Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- Title not available (Why is that?)
- Interpolation and SAT-based model checking.
- PeRIPLO: a framework for producing effective interpolants in SAT-based software verification
- SAT-Based Model Checking without Unrolling
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
- Lazy Abstraction with Interpolants
- Generalized property directed reachability
- Guiding Craig interpolation with domain-specific abstractions
- Accelerating interpolants
- Horn clauses for communicating timed systems
- SMT-based model checking for recursive programs
- ICE-based refinement type discovery for higher-order functional programs
- Tree automata-based refinement with application to Horn clause verification
- OpenSMT2: an SMT solver for multi-core and cloud computing
- A unifying view on SMT-based software verification
- Title not available (Why is that?)
- Learning inductive invariants by sampling from frequency distributions
- RustHorn: CHC-based verification for Rust programs
- Software verification with PDR: an implementation of the state of the art
- HoIce: an ICE-based non-linear Horn clause solver
- Title not available (Why is that?)
- Global guidance for local generalization in model checking
- Title not available (Why is that?)
- Transition power abstractions for deep counterexample detection
- Maximizing branch coverage with constrained Horn clauses
Cited In (1)
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)
