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
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)0302-9743
ISSN (Electronic)1611-3349

Other

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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Probabilistic abstract interpretation'. Together they form a unique fingerprint.

Cite this