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 (CEA) - 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
Contributor : Jean Goubault-Larrecq Connect in order to contact the contributor
Submitted on : Tuesday, February 4, 2014 - 4:58:31 PM
Last modification on : Thursday, February 17, 2022 - 10:08:03 AM
Long-term archiving on: : Sunday, April 9, 2017 - 8:50:46 AM


Files produced by the author(s)




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⟩



Record views


Files downloads