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

• Solving non-linear Horn clauses using a linear Horn clause solver
• Generalised interpolation by solving recursion-free Horn clauses
• IC3 -- flipping the E in ICE
• Automating induction for solving Horn clauses
• Horn clause solvers for program verification

Mathematics Subject Classification ID

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 (14)

• ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative 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
• 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
• Fold/Unfold Transformations for Fixpoint Logic
• RustHorn: CHC-Based Verification for Rust Programs
• Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes
• Learning inductive invariants by sampling from frequency distributions
• The \textsc{Golem} Horn solver

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)