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

DOI10.1007/978-3-030-02768-1_8zbMath1519.68045OpenAlexW2896700544MaRDI QIDQ6166141

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) Functional programming and lambda calculus (68N18) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (12)

RustHorn: CHC-Based Verification for Rust Programs ⋮ ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs ⋮ Loop verification with invariants and contracts ⋮ Unnamed Item ⋮ On higher-order reachability games vs may reachability ⋮ Solving constrained Horn clauses over algebraic data types ⋮ Learning inductive invariants by sampling from frequency distributions ⋮ Bridging arrays and ADTs in recursive proofs ⋮ Unbounded procedure summaries from bounded environments ⋮ Copy complexity of Horn formulas with respect to unit read-once resolution ⋮ Fold/Unfold Transformations for Fixpoint Logic ⋮ ICE-based refinement type discovery for higher-order functional programs

This page was built for publication: HoIce: an ICE-based non-linear Horn clause solver