Skip to Main content Skip to Navigation
Conference papers

Static Analysis of Programs with Imprecise Probabilistic Inputs

Assalé Adje 1, 2 Olivier Bouissou 3 Jean Goubault-Larrecq 1, 4 Eric Goubault 5 Sylvie Putot 5
3 LMeASI - Laboratoire Modélisation et Analyse de Systèmes en Interaction
LIST - Laboratoire d'Intégration des Systèmes et des Technologies : DRT/LIST
4 SECSI - Security of information systems
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
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.
Document type :
Conference papers
Complete list of metadata

Cited literature [41 references]  Display  Hide  Download

https://hal.inria.fr/hal-00942126
Contributor : Jean Goubault-Larrecq <>
Submitted on : Tuesday, February 4, 2014 - 4:58:31 PM
Last modification on : Friday, June 25, 2021 - 9:48:03 AM
Long-term archiving on: : Sunday, April 9, 2017 - 8:50:46 AM

File

main2.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Assalé Adje, Olivier Bouissou, Jean Goubault-Larrecq, Eric Goubault, Sylvie Putot. Static Analysis of Programs with Imprecise Probabilistic Inputs. VSTTE, May 2013, Snowbird, Utah, United States. pp.22-47, ⟨10.1007/978-3-642-54108-7⟩. ⟨hal-00942126⟩

Share

Metrics

Record views

532

Files downloads

558