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
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
- Title not available (Why is that?)
- 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
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)
