Bridging Boolean and Quantitative Synthesis Using Smoothed Proof Search

Swarat Chaudhuri 1 Martin Clochard 2, 3 Armando Solar-Lezama 4
2 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Abstract : We present a new technique for parameter synthesis under boolean and quantitative objectives. The input to the technique is a "sketch" - a program with missing numerical parameters - and a probabilistic assumption about the program's inputs. The goal is to automatically synthesize values for the parameters such that the resulting program satisfies: (1) a boolean specification, which states that the program must meet certain assertions, and (2) a quantitative specification, which assigns a real valued rating to every program and which the synthesizer is expected to optimize. Our method - called smoothed proof search - reduces this task to a sequence of unconstrained smooth optimization problems that are then solved numerically. By iteratively solving these problems, we obtain parameter values that get closer and closer to meeting the boolean specification; at the limit, we obtain values that provably meet the specification. The approximations are computed using a new notion of smoothing for program abstractions, where an abstract transformer is approximated by a function that is continuous according to a metric over abstract states. We present a prototype implementation of our synthesis procedure, and experimental results on two benchmarks from the embedded control domain. The experiments demonstrate the benefits of smoothed proof search over an approach that does not meet the boolean and quantitative synthesis goals simultaneously.
Type de document :
Communication dans un congrès
POPL - 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2014, San Diego, United States. ACM Press, 2014
Liste complète des métadonnées

https://hal.inria.fr/hal-00920955
Contributeur : Claude Marché <>
Soumis le : jeudi 19 décembre 2013 - 14:41:09
Dernière modification le : jeudi 9 février 2017 - 15:03:34
Document(s) archivé(s) le : jeudi 20 mars 2014 - 07:15:19

Fichier

clochard14popl.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00920955, version 1

Citation

Swarat Chaudhuri, Martin Clochard, Armando Solar-Lezama. Bridging Boolean and Quantitative Synthesis Using Smoothed Proof Search. POPL - 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2014, San Diego, United States. ACM Press, 2014. <hal-00920955>

Partager

Métriques

Consultations de
la notice

254

Téléchargements du document

160