HoIce: an ICE-based non-linear Horn clause solver

DOI10.1007/978-3-030-02768-1_8MaRDI QIDQ6166141zbMATH OpenOpenAlexFDO

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

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)

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

Cited in

(17)

• RustHorn: CHC-based verification for Rust programs
• ICE-based refinement type discovery for higher-order functional programs
• scientific article; zbMATH DE number 7589540 (Why is no real title available?)
• 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)