An assertion-based program logic for probabilistic programs

Gilles Barthe; Thomas Espitau; Marco Gaboardi; Benjamin Grégoire; Justin Hsu; Pierre Yves Strub

doi:10.1007/978-3-319-89884-1_5

An assertion-based program logic for probabilistic programs

Gilles Barthe
, Thomas Espitau
, Marco Gaboardi
, Benjamin Grégoire
, Justin Hsu
, Pierre Yves Strub

École Polytechnique

IMDEA Software Institute
Sorbonne Université
University at Buffalo, The State University of New York
INRIA
University College London

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

Résumé

We present Ellora, a sound and relatively complete assertion-based program logic, and demonstrate its expressivity by verifying several classical examples of randomized algorithms using an implementation in the EasyCrypt proof assistant. Ellora features new proof rules for loops and adversarial code, and supports richer assertions than existing program logics. We also show that Ellora allows convenient reasoning about complex probabilistic concepts by developing a new program logic for probabilistic independence and distribution law, and then smoothly embedding it into Ellora.

langue originale	Anglais
titre	Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings
rédacteurs en chef	Amal Ahmed
Editeur	Springer Verlag
Pages	117-144
Nombre de pages	28
ISBN (imprimé)	9783319898834
Les DOIs	https://doi.org/10.1007/978-3-319-89884-1_5
état	Publié - 1 janv. 2018
Evénement	27th European Symposium on Programming, ESOP 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018 - Thessaloniki, Grcce Durée: 14 avr. 2018 → 20 avr. 2018

Série de publications

Nom	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	10801 LNCS
ISSN (imprimé)	0302-9743
ISSN (Electronique)	1611-3349

Une conférence

Une conférence	27th European Symposium on Programming, ESOP 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018
Pays/Territoire	Grcce
La ville	Thessaloniki
période	14/04/18 → 20/04/18

Accès au document

10.1007/978-3-319-89884-1_5

Autres fichiers et liens

Lien vers la publication dans Scopus

Contient cette citation

Barthe, G., Espitau, T., Gaboardi, M., Grégoire, B., Hsu, J., & Strub, P. Y. (2018). An assertion-based program logic for probabilistic programs. Dans A. Ahmed (Ed.), Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings (p. 117-144). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol 10801 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-89884-1_5

Barthe, Gilles ; Espitau, Thomas ; Gaboardi, Marco et al. / An assertion-based program logic for probabilistic programs. Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings. Editeur / Amal Ahmed. Springer Verlag, 2018. p. 117-144 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{c2d881b955384836921bd4e3d7518504,

title = "An assertion-based program logic for probabilistic programs",

abstract = "We present Ellora, a sound and relatively complete assertion-based program logic, and demonstrate its expressivity by verifying several classical examples of randomized algorithms using an implementation in the EasyCrypt proof assistant. Ellora features new proof rules for loops and adversarial code, and supports richer assertions than existing program logics. We also show that Ellora allows convenient reasoning about complex probabilistic concepts by developing a new program logic for probabilistic independence and distribution law, and then smoothly embedding it into Ellora.",

author = "Gilles Barthe and Thomas Espitau and Marco Gaboardi and Benjamin Gr{\'e}goire and Justin Hsu and Strub, \{Pierre Yves\}",

note = "Publisher Copyright: {\textcopyright} The Author(s) 2018.; 27th European Symposium on Programming, ESOP 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018 ; Conference date: 14-04-2018 Through 20-04-2018",

year = "2018",

month = jan,

day = "1",

doi = "10.1007/978-3-319-89884-1\_5",

language = "English",

isbn = "9783319898834",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "117--144",

editor = "Amal Ahmed",

booktitle = "Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings",

}

Barthe, G, Espitau, T, Gaboardi, M, Grégoire, B, Hsu, J & Strub, PY 2018, An assertion-based program logic for probabilistic programs. Dans A Ahmed (Ed.), Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), VOL. 10801 LNCS, Springer Verlag, p. 117-144, 27th European Symposium on Programming, ESOP 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Grcce, 14/04/18. https://doi.org/10.1007/978-3-319-89884-1_5

An assertion-based program logic for probabilistic programs. / Barthe, Gilles; Espitau, Thomas; Gaboardi, Marco et al.
Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings. Ed. / Amal Ahmed. Springer Verlag, 2018. p. 117-144 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol 10801 LNCS).

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

TY - GEN

T1 - An assertion-based program logic for probabilistic programs

AU - Barthe, Gilles

AU - Espitau, Thomas

AU - Gaboardi, Marco

AU - Grégoire, Benjamin

AU - Hsu, Justin

AU - Strub, Pierre Yves

PY - 2018/1/1

Y1 - 2018/1/1

N2 - We present Ellora, a sound and relatively complete assertion-based program logic, and demonstrate its expressivity by verifying several classical examples of randomized algorithms using an implementation in the EasyCrypt proof assistant. Ellora features new proof rules for loops and adversarial code, and supports richer assertions than existing program logics. We also show that Ellora allows convenient reasoning about complex probabilistic concepts by developing a new program logic for probabilistic independence and distribution law, and then smoothly embedding it into Ellora.

AB - We present Ellora, a sound and relatively complete assertion-based program logic, and demonstrate its expressivity by verifying several classical examples of randomized algorithms using an implementation in the EasyCrypt proof assistant. Ellora features new proof rules for loops and adversarial code, and supports richer assertions than existing program logics. We also show that Ellora allows convenient reasoning about complex probabilistic concepts by developing a new program logic for probabilistic independence and distribution law, and then smoothly embedding it into Ellora.

UR - https://www.scopus.com/pages/publications/85045623167

U2 - 10.1007/978-3-319-89884-1_5

DO - 10.1007/978-3-319-89884-1_5

M3 - Conference contribution

AN - SCOPUS:85045623167

SN - 9783319898834

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 117

EP - 144

BT - Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings

A2 - Ahmed, Amal

PB - Springer Verlag

T2 - 27th European Symposium on Programming, ESOP 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018

Y2 - 14 April 2018 through 20 April 2018

ER -

Barthe G, Espitau T, Gaboardi M, Grégoire B, Hsu J, Strub PY. An assertion-based program logic for probabilistic programs. Dans Ahmed A, Editeur, Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings. Springer Verlag. 2018. p. 117-144. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-89884-1_5

An assertion-based program logic for probabilistic programs

Résumé

Série de publications

Une conférence

Accès au document

Autres fichiers et liens

Empreinte digitale

Contient cette citation