Bridging boolean and quantitative synthesis using smoothed proof search

DOI10.1145/2535838.2535859zbMath1284.68169OpenAlexW3014235357MaRDI QIDQ5408417

Swarat Chaudhuri, Armando Solar-Lezama, Martin Clochard

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

synthesisabstract interpretationprobabilistic verificationprobabilistic programsprogram smoothing

Mathematics Subject Classification ID

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

Related Items (3)

Continualization of Probabilistic Programs With Correction ⋮ Counterexample-guided inductive synthesis for probabilistic systems ⋮ Automated formal synthesis of provably safe digital controllers for continuous plants

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