ICE-based refinement type discovery for higher-order functional programs
From MaRDI portal
Publication:5919615
DOI10.1007/978-3-319-89960-2_20zbMath1468.68058OpenAlexW2798232457MaRDI QIDQ5919615
Adrien Champion, Naoki Kobayashi, Ryosuke Sato, Tomoya Chiba
Publication date: 16 September 2019
Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-89960-2_20
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 (7)
RustHorn: CHC-Based Verification for Rust Programs ⋮ Constraint-based relational verification ⋮ Decision tree learning in CEGIS-based termination analysis ⋮ Solving constrained Horn clauses over algebraic data types ⋮ A learning-based approach to synthesizing invariants for incomplete verification engines ⋮ Predicate abstraction and CEGAR for \(\nu \mathrm{HFL}_\mathbb{Z}\) validity checking ⋮ ICE-based refinement type discovery for higher-order functional programs
This page was built for publication: ICE-based refinement type discovery for higher-order functional programs