Counterexample-guided partial bounding for recursive function synthesis

DOI10.1007/978-3-030-81685-8_39MaRDI QIDQ832233zbMATH OpenOpenAlexFDO

Authors Azadeh Farzan, Victor Nicolet

Publication date 25 March 2022

Copyright license Creative Commons Attribution 4.0 International

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

Mathematics Subject Classification ID

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

Recommendations

• Counterexample-guided quantifier instantiation for synthesis in SMT
• Synthesis with asymptotic resource bounds
• Counterexample guided inductive synthesis modulo theories
• scientific article; zbMATH DE number 4020482
• scientific article; zbMATH DE number 4049027

Cites work

• A Methodology for LISP Program Construction from Examples
• A Transformation System for Developing Recursive Programs
• A type-directed abstraction refinement approach to higher-order model checking
• Automatic parallelization of recursive functions using quantifier elimination
• Automatically Introducing Tail Recursion in CakeML
• Bounded quantifier instantiation for checking inductive invariants
• Counterexample-guided quantifier instantiation for synthesis in SMT
• Example-directed synthesis: a type-theoretic interpretation
• Higher-order multi-parameter tree transducers and recursion schemes for program verification
• Inductive synthesis of functional programs: an explanation based generalization approach
• Synthesis of recursive ADT transformations from reusable templates
• The third homomorphism theorem on trees: downward \& upward lead to divide-and-conquer
• Types and higher-order recursion schemes for verification of higher-order programs
• Verifying higher-order functional programs with pattern-matching algebraic data types

Cited in

(2)

• Synthesis with asymptotic resource bounds
• Preface of the special issue on the conference on computer-aided verification 2020 and 2021

Describes a project that uses

Uses Software

• GitHub
• MoCHi
• CVC4
• OCaml
• z3

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)