ICE-based refinement type discovery for higher-order functional programs

DOI10.1007/S10817-020-09571-YzbMath1468.68059OpenAlexW3046473740MaRDI QIDQ5919002

Naoki Kobayashi, Adrien Champion, Tomoya Chiba, Ryosuke Sato

Publication date: 2 November 2020

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-020-09571-y

zbMATH Keywords

formal verificationmachine learningrefinement typeshigher-order program verification

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

Toward neural-network-guided program synthesis and verification ⋮ Symbolic automatic relations and their applications to SMT and CHC solving ⋮ Analysis and Transformation of Constrained Horn Clauses for Program Verification ⋮ Parameterized recursive refinement types for automated program verification ⋮ Efficient modular SMT-based model checking of pointer programs ⋮ On higher-order reachability games vs may reachability ⋮ Reasoning About Data Trees Using CHCs ⋮ Termination Analysis for the $$\pi $$-Calculus by Reduction to Sequential Program Termination

Uses Software

• FLATA
• z3
• Princess
• Eldarica
• HMC
• c2i
• Spacer
• Kind 2

Cites Work

• Unnamed Item
• Unnamed Item
• SMT-based model checking for recursive programs
• From invariant checking to invariant inference using randomized search
• Tools and algorithms for the construction and analysis of systems. 18th international conference, TACAS 2012, held as part of the European joint conferences on theory and practice of software, ETAPS 2012, Tallinn, Estonia, March 24 -- April 1, 2012. Proceedings
• Generalized Property Directed Reachability
• Compositional and Lightweight Dependent Type Inference for ML
• Automating relatively complete verification of higher-order functional programs
• Horn Clause Solvers for Program Verification
• Learning refinement types
• SAT-Based Model Checking without Unrolling
• Solving Horn Clauses on Inductive Data Types Without Induction
• Dependent Array Type Inference from Tests
• Dependent types from counterexamples
• Low-level liquid types
• Computational Complexity
• A Data Driven Approach for Algebraic Loop Invariants
• Automatic Termination Verification for Higher-Order Functional Programs
• ICE-based refinement type discovery for higher-order functional programs
• HoIce: an ICE-based non-linear Horn clause solver

This page was built for publication: ICE-based refinement type discovery for higher-order functional programs