HoIce: an ICE-based non-linear Horn clause solver
DOI10.1007/978-3-030-02768-1_8zbMATH Open1519.68045OpenAlexW2896700544MaRDI QIDQ6166141FDOQ6166141
Authors: Adrien Champion, Naoki Kobayashi, Ryosuke Sato 
Publication date: 2 August 2023
Published in: Programming Languages and Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-030-02768-1_8
Recommendations
Learning and adaptive systems in artificial intelligence (68T05) Specification and verification (program logics, model checking, etc.) (68Q60) Functional programming and lambda calculus (68N18)
Cited In (17)
- RustHorn: CHC-based verification for Rust programs
- ICE-based refinement type discovery for higher-order functional programs
- Title not available (Why is that?)
- ICE-based refinement type discovery for higher-order functional programs
- Unbounded procedure summaries from bounded environments
- Copy complexity of Horn formulas with respect to unit read-once resolution
- IC3 -- flipping the E in ICE
- On higher-order reachability games vs may reachability
- Solving constrained Horn clauses over algebraic data types
- Bridging arrays and ADTs in recursive proofs
- Loop verification with invariants and contracts
- ConSORT: context- and flow-sensitive ownership refinement types for imperative programs
- Solving non-linear Horn clauses using a linear Horn clause solver
- Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes
- Learning inductive invariants by sampling from frequency distributions
- The \textsc{Golem} Horn solver
- Fold/unfold transformations for fixpoint logic
This page was built for publication: HoIce: an ICE-based non-linear Horn clause solver
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6166141)
