Synthesis with asymptotic resource bounds

DOI10.1007/978-3-030-81685-8_37zbMATH Open1493.68112arXiv2103.04188OpenAlexW3186139944MaRDI QIDQ832230FDOQ832230

Authors: Qinheping Hu, John Cyphert, Loris D'Antoni, Thomas Reps 

Publication date: 25 March 2022

Abstract: We present a method for synthesizing recursive functions that satisfy both a functional specification and an asymptotic resource bound. Prior methods for synthesis with a resource metric require the user to specify a concrete expression exactly describing resource usage, whereas our method uses big-O notation to specify the asymptotic resource usage. Our method can synthesize programs with complex resource bounds, such as a sort function that has complexity O(nlog(n)). Our synthesis procedure uses a type system that is able to assign an asymptotic complexity to terms, and can track recurrence relations of functions. These typing rules are justified by theorems used in analysis of algorithms, such as the Master Theorem and the Akra-Bazzi method. We implemented our method as an extension of prior type-based synthesis work. Our tool, SynPlexity, was able to synthesize complex divide-and-conquer programs that cannot be synthesized by prior solvers.

Full work available at URL: https://arxiv.org/abs/2103.04188

Recommendations

• From program verification to program synthesis
• Counterexample-guided partial bounding for recursive function synthesis
• scientific article; zbMATH DE number 4049027
• scientific article; zbMATH DE number 4020482
• Non-polynomial worst-case analysis of recursive programs

Mathematics Subject Classification ID

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

Cites Work

• Introduction to algorithms.
• Multivariate amortized resource analysis
• On the solution of linear recurrence equations
• The concrete tetrahedron. Symbolic sums, recurrence equations, generating functions, asymptotic estimates
• Closed-form upper bounds in static cost analysis
• Mechanical program analysis
• Title not available (Why is that?)
• Exponential automatic amortized resource analysis
• A fistful of dollars: formalizing asymptotic complexity claims via deductive program verification
• Proving divide and conquer complexities in Isabelle/HOL
• Syntax-guided synthesis with quantitative syntactic objectives

Cited In (2)

• Computing unrestricted synopses under maximum error bound
• Programmable program synthesis

Uses Software

• TiML

This page was built for publication: Synthesis with asymptotic resource bounds

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q832230)