Static analysis of programs with imprecise probabilistic inputs

Assale Adje; Olivier Bouissou; Jean Goubault-Larrecq; Eric Goubault; Sylvie Putot

doi:10.1007/978-3-642-54108-7_2

Static analysis of programs with imprecise probabilistic inputs

Assale Adje
, Olivier Bouissou
, Jean Goubault-Larrecq
, Eric Goubault
, Sylvie Putot

ENS Paris-Saclay
Institut Pierre Simon Laplace, CNRS and CEA

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

Having a precise yet sound abstraction of the inputs of numerical programs is important to analyze their behavior. For many programs, these inputs are probabilistic, but the actual distribution used is only partially known. We present a static analysis framework for reasoning about programs with inputs given as imprecise probabilities: we define a collecting semantics based on the notion of previsions and an abstract semantics based on an extension of Dempster-Shafer structures. We prove the correctness of our approach and show on some realistic examples the kind of invariants we are able to infer.

Original language	English
Title of host publication	Verified Software
Subtitle of host publication	Theories, Tools, Experiments - 5th International Conference, VSTTE 2013, Revised Selected Papers
Editors	Ernie Cohen, Andrey Rybalchenko, Andrey Rybalchenko
Publisher	Springer Verlag
Pages	22-47
Number of pages	26
ISBN (Electronic)	9783642541070
DOIs	https://doi.org/10.1007/978-3-642-54108-7_2
Publication status	Published - 1 Jan 2014
Externally published	Yes
Event	5th International Conference on Verified Software: Theories, Tools, Experiments, VSTTE 2013 - Menlo Park, United States Duration: 17 May 2013 → 19 May 2013

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	8164
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	5th International Conference on Verified Software: Theories, Tools, Experiments, VSTTE 2013
Country/Territory	United States
City	Menlo Park
Period	17/05/13 → 19/05/13

Access to Document

10.1007/978-3-642-54108-7_2

Cite this

Adje, A., Bouissou, O., Goubault-Larrecq, J., Goubault, E., & Putot, S. (2014). Static analysis of programs with imprecise probabilistic inputs. In E. Cohen, A. Rybalchenko, & A. Rybalchenko (Eds.), Verified Software: Theories, Tools, Experiments - 5th International Conference, VSTTE 2013, Revised Selected Papers (pp. 22-47). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8164). Springer Verlag. https://doi.org/10.1007/978-3-642-54108-7_2

Adje, Assale ; Bouissou, Olivier ; Goubault-Larrecq, Jean et al. / Static analysis of programs with imprecise probabilistic inputs. Verified Software: Theories, Tools, Experiments - 5th International Conference, VSTTE 2013, Revised Selected Papers. editor / Ernie Cohen ; Andrey Rybalchenko ; Andrey Rybalchenko. Springer Verlag, 2014. pp. 22-47 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{9f59dcc022274233a0ebab824eca5094,

title = "Static analysis of programs with imprecise probabilistic inputs",

abstract = "Having a precise yet sound abstraction of the inputs of numerical programs is important to analyze their behavior. For many programs, these inputs are probabilistic, but the actual distribution used is only partially known. We present a static analysis framework for reasoning about programs with inputs given as imprecise probabilities: we define a collecting semantics based on the notion of previsions and an abstract semantics based on an extension of Dempster-Shafer structures. We prove the correctness of our approach and show on some realistic examples the kind of invariants we are able to infer.",

author = "Assale Adje and Olivier Bouissou and Jean Goubault-Larrecq and Eric Goubault and Sylvie Putot",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 2014.; 5th International Conference on Verified Software: Theories, Tools, Experiments, VSTTE 2013 ; Conference date: 17-05-2013 Through 19-05-2013",

year = "2014",

month = jan,

day = "1",

doi = "10.1007/978-3-642-54108-7\_2",

language = "English",

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

publisher = "Springer Verlag",

pages = "22--47",

editor = "Ernie Cohen and Andrey Rybalchenko and Andrey Rybalchenko",

booktitle = "Verified Software",

}

Adje, A, Bouissou, O, Goubault-Larrecq, J, Goubault, E & Putot, S 2014, Static analysis of programs with imprecise probabilistic inputs. in E Cohen, A Rybalchenko & A Rybalchenko (eds), Verified Software: Theories, Tools, Experiments - 5th International Conference, VSTTE 2013, Revised Selected Papers. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8164, Springer Verlag, pp. 22-47, 5th International Conference on Verified Software: Theories, Tools, Experiments, VSTTE 2013, Menlo Park, United States, 17/05/13. https://doi.org/10.1007/978-3-642-54108-7_2

Static analysis of programs with imprecise probabilistic inputs. / Adje, Assale; Bouissou, Olivier; Goubault-Larrecq, Jean et al.
Verified Software: Theories, Tools, Experiments - 5th International Conference, VSTTE 2013, Revised Selected Papers. ed. / Ernie Cohen; Andrey Rybalchenko; Andrey Rybalchenko. Springer Verlag, 2014. p. 22-47 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8164).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Static analysis of programs with imprecise probabilistic inputs

AU - Adje, Assale

AU - Bouissou, Olivier

AU - Goubault-Larrecq, Jean

AU - Goubault, Eric

AU - Putot, Sylvie

PY - 2014/1/1

Y1 - 2014/1/1

N2 - Having a precise yet sound abstraction of the inputs of numerical programs is important to analyze their behavior. For many programs, these inputs are probabilistic, but the actual distribution used is only partially known. We present a static analysis framework for reasoning about programs with inputs given as imprecise probabilities: we define a collecting semantics based on the notion of previsions and an abstract semantics based on an extension of Dempster-Shafer structures. We prove the correctness of our approach and show on some realistic examples the kind of invariants we are able to infer.

AB - Having a precise yet sound abstraction of the inputs of numerical programs is important to analyze their behavior. For many programs, these inputs are probabilistic, but the actual distribution used is only partially known. We present a static analysis framework for reasoning about programs with inputs given as imprecise probabilities: we define a collecting semantics based on the notion of previsions and an abstract semantics based on an extension of Dempster-Shafer structures. We prove the correctness of our approach and show on some realistic examples the kind of invariants we are able to infer.

U2 - 10.1007/978-3-642-54108-7_2

DO - 10.1007/978-3-642-54108-7_2

M3 - Conference contribution

AN - SCOPUS:84908652171

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

SP - 22

EP - 47

BT - Verified Software

A2 - Cohen, Ernie

A2 - Rybalchenko, Andrey

PB - Springer Verlag

T2 - 5th International Conference on Verified Software: Theories, Tools, Experiments, VSTTE 2013

Y2 - 17 May 2013 through 19 May 2013

ER -

Adje A, Bouissou O, Goubault-Larrecq J, Goubault E , Putot S. Static analysis of programs with imprecise probabilistic inputs. In Cohen E, Rybalchenko A, Rybalchenko A, editors, Verified Software: Theories, Tools, Experiments - 5th International Conference, VSTTE 2013, Revised Selected Papers. Springer Verlag. 2014. p. 22-47. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-54108-7_2

Static analysis of programs with imprecise probabilistic inputs

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this