Bridging Boolean and quantitative synthesis using smoothed proof search

DOI10.1145/2535838.2535859MaRDI QIDQ5408417zbMATH OpenOpenAlexFDO

Authors Swarat Chaudhuri, Martin Clochard, Armando Solar-Lezama

Publication date 10 April 2014

Published in Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2535838.2535859

zbMATH Keywords

abstract interpretationprobabilistic programsprobabilistic verificationprogram smoothingsynthesis

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Recommendations

• Synthesis in pMDPs: a tale of 1001 parameters
• Boolean functional synthesis: hardness and practical algorithms
• Parameter synthesis for Markov models: faster than ever
• What's hard about Boolean functional synthesis?
• From program verification to program synthesis

Cited in

(4)

• Counterexample-guided inductive synthesis for probabilistic systems
• Automated formal synthesis of provably safe digital controllers for continuous plants
• Continualization of probabilistic programs with correction
• Quantitative program sketching using lifted static analysis

This page was built for publication: Bridging Boolean and quantitative synthesis using smoothed proof search

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