Abstract
The goal of probabilistic static analysis is to quantify the probability that a given program satisfies/violates a required property (assertion). In this work, we use a static analysis by abstract interpretation and model counting to construct probabilistic analysis of deterministic programs with uncertain input data, which can be used for estimating the probabilities of assertions (program reliability).
In particular, we automatically infer necessary preconditions in order a given assertion to be satisfied/violated at run-time using a combination of forward and backward static analyses. The focus is on numeric properties of variables and numeric abstract domains, such as polyhedra. The obtained preconditions in the form of linear constraints are then analyzed to quantify how likely is an input to satisfy them. Model counting techniques are employed to count the number of solutions that satisfy given linear constraints. These counts are then used to assess the probability that the target assertion is satisfied/violated. We also present how to extend our approach to analyze non-deterministic programs by inferring sufficient preconditions. We built a prototype implementation and evaluate it on several interesting examples.
Chapter PDF
Similar content being viewed by others
References
Latte integrale. UC Davis, Mathematics.
Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008.
Mateus Borges, Antonio Filieri, Marcelo d’Amorim, Corina S. Pasareanu, and Willem Visser. Compositional solution space quantification for probabilistic software analysis. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI’14, page 15. ACM, 2014.
François Bourdoncle. Abstract debugging of higher-order imperative languages. In Proceedings of the ACM SIGPLAN’93 Conference on Programming Language Design and Implementation (PLDI), pages 46–55. ACM, 1993.
N. V. Chernikova. Algorithm for finding a general formula for the non-negative solutions of a system of linear inequalities. USSR Computational Mathematics and Mathematical Physics, 5(2):228–233, 1965.
Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth ACM Symposium on Principles of Programming Languages (POPL’77), pages 238–252. ACM, 1977.
Patrick Cousot and Radhia Cousot. Systematic design of program analysis frameworks. In 6th Annual ACM Symposium on Principles of Programming Languages, POPL ’79, pages 269–282, 1979.
Patrick Cousot and Radhia Cousot. Abstract interpretation and application to logic programs. J. Log. Program., 13(2–3):103–179, 1992.
Patrick Cousot, Radhia Cousot, and Francesco Logozzo. Precondition inference from intermittent assertions and application to contracts on collections. In Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011. Proceedings, volume 6538 of LNCS, pages 150–168. Springer, 2011.
Patrick Cousot and Nicolas Halbwachs. Automatic discovery of linear restraints among variables of a program. In Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages (POPL’78), pages 84–96. ACM Press, 1978.
Patrick Cousot and Michael Monerau. 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, volume 7211 of LNCS, pages 169–193. Springer, 2012.
Aleksandar S. Dimovski. Program verification using symbolic game semantics. Theor. Comput. Sci., 560:364–379, 2014.
Aleksandar S. Dimovski. Probabilistic analysis based on symbolic game semantics and model counting. In Proceedings Eighth International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2017, Roma, Italy, 20–22 September 2017., volume 256 of EPTCS, pages 1–15, 2017.
Aleksandar S. Dimovski. Lifted static analysis using a binary decision diagram abstract domain. In Proceedings of the 18th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, GPCE 2019, pages 102–114. ACM, 2019.
Aleksandar S. Dimovski, Claus Brabrand, and Andrzej Wasowski. Variability abstractions: Trading precision for speed in family-based analyses. In 29th European Conf. on Object-Oriented Programming, ECOOP 2015, volume 37 of LIPIcs, pages 247–270. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015.
Aleksandar S. Dimovski, Claus Brabrand, and Andrzej Wasowski. Finding suitable variability abstractions for lifted analysis. Formal Asp. Comput., 31(2):231–259, 2019.
Antonio Filieri, Corina S. Pasareanu, and Willem Visser. Reliability analysis in symbolic pathfinder. In 35th International Conference on Software Engineering, ICSE’13, pages 622–631. IEEE / ACM, 2013.
Jaco Geldenhuys, Matthew B. Dwyer, and Willem Visser. Probabilistic symbolic execution. In International Symposium on Software Testing and Analysis, ISSTA 2012, pages 166–176. ACM, 2012.
Andrew D. Gordon, Thomas A. Henzinger, Aditya V. Nori, and Sriram K. Rajamani. Probabilistic programming. In Proceedings of the on Future of Software Engineering, FOSE 2014, pages 167–181. ACM, 2014.
Bertrand Jeannet. Dynamic partitioning in linear relation analysis: Application to the verification of reactive systems. Formal Methods in System Design, 23(1):5–37, 2003.
Bertrand Jeannet and Antoine Miné. Apron: A library of numerical abstract domains for static analysis. In Computer Aided Verification, 21st International Conference, CAV 2009. Proceedings, volume 5643 of LNCS, pages 661–667. Springer, 2009.
Joost-Pieter Katoen, Annabelle McIver, Larissa Meinicke, and Carroll C. Morgan. Linear-invariant generation for probabilistic programs: - automated support for proof-based methods. In Static Analysis - 17th International Symposium, SAS 2010. Proceedings, volume 6337 of LNCS, pages 390–406. Springer, 2010.
Annabelle McIver and Carroll Morgan. Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer, 2005.
Jan Midtgaard, Aleksandar S. Dimovski, Claus Brabrand, and Andrzej Wasowski. Systematic derivation of correct variability-aware program analyses. Sci. Comput. Program., 105:145–170, 2015.
Antoine Miné. The octagon abstract domain. Higher-Order and Symbolic Computation, 19(1):31–100, 2006.
Antoine Miné. Backward under-approximations in numeric abstract domains to automatically infer sufficient program conditions. Sci. Comput. Program., 93:154–182, 2014.
David Monniaux. An abstract monte-carlo method for the analysis of probabilistic programs. In Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 93–101. ACM, 2001.
Xavier Rival. Understanding the origin of alarms in astrée. In Static Analysis, 12th International Symposium, SAS 2005, Proceedings, volume 3672 of LNCS, pages 303–319. Springer, 2005.
Sriram Sankaranarayanan, Aleksandar Chakarov, and Sumit Gulwani. Static analysis for probabilistic programs: inferring whole program properties from finitely many paths. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’13, pages 447–458. ACM, 2013.
Caterina Urban and Antoine Miné. A decision tree abstract domain for proving conditional termination. In Static Analysis - 21st International Symposium, SAS 2014. Proceedings, volume 8723 of LNCS, pages 302–318. Springer, 2014.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2020 The Author(s)
About this paper
Cite this paper
Dimovski, A.S., Legay, A. (2020). Computing Program Reliability Using Forward-Backward Precondition Analysis and Model Counting. In: Wehrheim, H., Cabot, J. (eds) Fundamental Approaches to Software Engineering. FASE 2020. Lecture Notes in Computer Science(), vol 12076. Springer, Cham. https://doi.org/10.1007/978-3-030-45234-6_9
Download citation
DOI: https://doi.org/10.1007/978-3-030-45234-6_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-45233-9
Online ISBN: 978-3-030-45234-6
eBook Packages: Computer ScienceComputer Science (R0)