Counterexample-guided partial bounding for recursive function synthesis
From MaRDI portal
Publication:832233
DOI10.1007/978-3-030-81685-8_39zbMATH Open1493.68107OpenAlexW3185895498MaRDI QIDQ832233FDOQ832233
Authors: Azadeh Farzan, Victor Nicolet 
Publication date: 25 March 2022
Full work available at URL: https://doi.org/10.1007/978-3-030-81685-8_39
Recommendations
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Functional programming and lambda calculus (68N18)
Cites Work
- A Transformation System for Developing Recursive Programs
- Types and higher-order recursion schemes for verification of higher-order programs
- A Methodology for LISP Program Construction from Examples
- Higher-order multi-parameter tree transducers and recursion schemes for program verification
- Verifying higher-order functional programs with pattern-matching algebraic data types
- Counterexample-guided quantifier instantiation for synthesis in SMT
- Example-directed synthesis: a type-theoretic interpretation
- Inductive synthesis of functional programs: an explanation based generalization approach
- Bounded quantifier instantiation for checking inductive invariants
- Synthesis of recursive ADT transformations from reusable templates
- Automatic parallelization of recursive functions using quantifier elimination
- Automatically Introducing Tail Recursion in CakeML
- The third homomorphism theorem on trees: downward \& upward lead to divide-and-conquer
- A type-directed abstraction refinement approach to higher-order model checking
Cited In (2)
Uses Software
This page was built for publication: Counterexample-guided partial bounding for recursive function synthesis
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q832233)
