Efficient synthesis with probabilistic constraints

DOI10.1007/978-3-030-25540-4_15MaRDI QIDQ6194578zbMATH OpenOpenAlexFDO

Authors Samuel Drews, Aws Albarghouthi, Loris D'Antoni

Publication date 16 February 2024

Published in Computer Aided Verification (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

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

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: We consider the problem of synthesizing a program given a probabilistic specification of its desired behavior. Specifically, we study the recent paradigm of distribution-guided inductive synthesis (DIGITS), which iteratively calls a synthesizer on finite sample sets from a given distribution. We make theoretical and algorithmic contributions: (i) We prove the surprising result that DIGITS only requires a polynomial number of synthesizer calls in the size of the sample set, despite its ostensibly exponential behavior. (ii) We present a property-directed version of DIGITS that further reduces the number of synthesizer calls, drastically improving synthesis performance on a range of benchmarks.

Recommendations

• Counterexample-driven synthesis for probabilistic program sketches
• Counterexample-guided inductive synthesis for probabilistic systems
• Inductive synthesis for probabilistic programs reaches new horizons
• From program verification to program synthesis
• Programmable program synthesis

Cited in

(2)

• Symbolic execution + model counting + entropy maximization = automatic search synthesis
• Counterexample-driven synthesis for probabilistic program sketches

This page was built for publication: Efficient synthesis with probabilistic constraints

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