Counterexample-guided partial bounding for recursive function synthesis

DOI10.1007/978-3-030-81685-8_39zbMath1493.68107OpenAlexW3185895498MaRDI QIDQ832233

Victor Nicolet, Azadeh Farzan

Publication date: 25 March 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-81685-8_39

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Uses Software

• z3
• OCaml
• CVC4
• MoCHi
• GitHub

Cites Work

• Unnamed Item
• Counterexample-guided quantifier instantiation for synthesis in SMT
• Example-directed synthesis: a type-theoretic interpretation
• Bounded Quantifier Instantiation for Checking Inductive Invariants
• Synthesis of Recursive ADT Transformations from Reusable Templates
• Automatic Parallelization of Recursive Functions Using Quantifier Elimination
• A Methodology for LISP Program Construction from Examples
• A Transformation System for Developing Recursive Programs
• Automatically Introducing Tail Recursion in CakeML
• Higher-order multi-parameter tree transducers and recursion schemes for program verification
• The third homomorphism theorem on trees
• Types and higher-order recursion schemes for verification of higher-order programs
• A type-directed abstraction refinement approach to higher-order model checking
• Verifying higher-order functional programs with pattern-matching algebraic data types

This page was built for publication: Counterexample-guided partial bounding for recursive function synthesis