Probabilistic abstract interpretation

Patrick Cousot, Michael Monerau

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Abstract interpretation has been widely used for verifying properties of computer systems. Here, we present a way to extend this framework to the case of probabilistic systems. The probabilistic abstraction framework that we propose allows us to systematically lift any classical analysis or verification method to the probabilistic setting by separating in the program semantics the probabilistic behavior from the (non-)deterministic behavior. This separation provides new insights for designing novel probabilistic static analyses and verification methods. We define the concrete probabilistic semantics and propose different ways to abstract them. We provide examples illustrating the expressiveness and effectiveness of our approach.

Original languageEnglish (US)
Title of host publicationProgramming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Proceedings
Pages169-193
Number of pages25
Volume7211 LNCS
DOIs
StatePublished - 2012
Event21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012 - Tallinn, Estonia
Duration: Mar 24 2012Apr 1 2012

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7211 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012
CountryEstonia
CityTallinn
Period3/24/124/1/12

Fingerprint

Abstract Interpretation
Semantics
Computer systems
Concretes
Expressiveness

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Cousot, P., & Monerau, M. (2012). Probabilistic abstract interpretation. In Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Proceedings (Vol. 7211 LNCS, pp. 169-193). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7211 LNCS). https://doi.org/10.1007/978-3-642-28869-2_9

Probabilistic abstract interpretation. / Cousot, Patrick; Monerau, Michael.

Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Proceedings. Vol. 7211 LNCS 2012. p. 169-193 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7211 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Cousot, P & Monerau, M 2012, Probabilistic abstract interpretation. in Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Proceedings. vol. 7211 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7211 LNCS, pp. 169-193, 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, 3/24/12. https://doi.org/10.1007/978-3-642-28869-2_9
Cousot P, Monerau M. Probabilistic abstract interpretation. In Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Proceedings. Vol. 7211 LNCS. 2012. p. 169-193. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-28869-2_9
Cousot, Patrick ; Monerau, Michael. / Probabilistic abstract interpretation. Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Proceedings. Vol. 7211 LNCS 2012. pp. 169-193 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{96117d44268943e99de8f924a6801700,
title = "Probabilistic abstract interpretation",
abstract = "Abstract interpretation has been widely used for verifying properties of computer systems. Here, we present a way to extend this framework to the case of probabilistic systems. The probabilistic abstraction framework that we propose allows us to systematically lift any classical analysis or verification method to the probabilistic setting by separating in the program semantics the probabilistic behavior from the (non-)deterministic behavior. This separation provides new insights for designing novel probabilistic static analyses and verification methods. We define the concrete probabilistic semantics and propose different ways to abstract them. We provide examples illustrating the expressiveness and effectiveness of our approach.",
author = "Patrick Cousot and Michael Monerau",
year = "2012",
doi = "10.1007/978-3-642-28869-2_9",
language = "English (US)",
isbn = "9783642288685",
volume = "7211 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "169--193",
booktitle = "Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Proceedings",

}

TY - GEN

T1 - Probabilistic abstract interpretation

AU - Cousot, Patrick

AU - Monerau, Michael

PY - 2012

Y1 - 2012

N2 - Abstract interpretation has been widely used for verifying properties of computer systems. Here, we present a way to extend this framework to the case of probabilistic systems. The probabilistic abstraction framework that we propose allows us to systematically lift any classical analysis or verification method to the probabilistic setting by separating in the program semantics the probabilistic behavior from the (non-)deterministic behavior. This separation provides new insights for designing novel probabilistic static analyses and verification methods. We define the concrete probabilistic semantics and propose different ways to abstract them. We provide examples illustrating the expressiveness and effectiveness of our approach.

AB - Abstract interpretation has been widely used for verifying properties of computer systems. Here, we present a way to extend this framework to the case of probabilistic systems. The probabilistic abstraction framework that we propose allows us to systematically lift any classical analysis or verification method to the probabilistic setting by separating in the program semantics the probabilistic behavior from the (non-)deterministic behavior. This separation provides new insights for designing novel probabilistic static analyses and verification methods. We define the concrete probabilistic semantics and propose different ways to abstract them. We provide examples illustrating the expressiveness and effectiveness of our approach.

UR - http://www.scopus.com/inward/record.url?scp=84859141593&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84859141593&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-28869-2_9

DO - 10.1007/978-3-642-28869-2_9

M3 - Conference contribution

AN - SCOPUS:84859141593

SN - 9783642288685

VL - 7211 LNCS

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

SP - 169

EP - 193

BT - Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Proceedings

ER -