Calvin Smith
Skip Abstract Section
Skip Supplemental Material SectionAbstract
We propose trace abstraction modulo probability, a proof technique for verifying high-probability accuracy guarantees of probabilistic programs. Our proofs overapproximate the set of program traces using failure automata, finite-state automata that upper bound the probability of failing to satisfy a target specification. We automate proof construction by reducing probabilistic reasoning to logical reasoning: we use program synthesis methods to select axioms for sampling instructions, and then apply Craig interpolation to prove that traces fail the target specification with only a small probability. Our method handles programs with unknown inputs, parameterized distributions, infinite state spaces, and parameterized specifications. We evaluate our technique on a range of randomized algorithms drawn from the differential privacy literature and beyond. To our knowledge, our approach is the first to automatically establish accuracy properties of these algorithms.
Supplemental Material
- John M. Abowd and Ian M. Schmutte. 2017. Revisiting the Economics of Privacy: Population Statistics and Confidentiality Protection as Public Goods. Technical Report 17–37. Center for Economic Studies.Google Scholar
- Aws Albarghouthi. 2017. Probabilistic Horn Clause Verification. In International Symposium on Static Analysis (SAS), New York, New York. 1–22.Google Scholar
- Aws Albarghouthi, Loris D’Antoni, Samuel Drews, and Aditya V Nori. 2017. FairSquare: probabilistic verification of program fairness. Proceedings of the ACM on Programming Languages 1, OOPSLA (2017), 80. Google ScholarDigital Library
- Aws Albarghouthi, Arie Gurfinkel, and Marsha Chechik. 2012. Whale: An interpolation-based algorithm for inter-procedural verification. In International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), Philadelphia, Pennsylvania. Springer-Verlag, 39–55. Google ScholarDigital Library
- Aws Albarghouthi and Justin Hsu. 2018a. Constraint-Based Synthesis of Coupling Proofs. In International Conference on Computer Aided Verification (CAV), Oxford, England.Google Scholar
- Aws Albarghouthi and Justin Hsu. 2018b. Synthesizing coupling proofs of differential privacy. Proceedings of the ACM on Programming Languages 2, POPL (2018), 58:1–58:30. Google ScholarDigital Library
- Aws Albarghouthi and Kenneth L. McMillan. 2013. Beautiful interpolants. In International Conference on Computer Aided Verification (CAV), Saint Petersburg, Russia. Springer, 313–329.Google Scholar
- Christel Baier, Luca de Alfaro, Vojtech Forejt, and Marta Kwiatkowska. 2018. Model Checking Probabilistic Systems. In Handbook of Model Checking. Springer-Verlag, 963–999.Google Scholar
- Thomas Ball and Sriram K Rajamani. 2001. Automatically validating temporal safety properties of interfaces. In International SPIN Workshop on Model Checking of Software, Toronto, Ontario. Springer-Verlag, 103–122. Google ScholarDigital Library
- Gilles Barthe, Thomas Espitau, Luis María Ferrer Fioriti, and Justin Hsu. 2016a. Synthesizing Probabilistic Invariants via Doob’s Decomposition. In International Conference on Computer Aided Verification (CAV), Toronto, Ontario (Lecture Notes in Computer Science), Vol. 9779. Springer-Verlag, 43–61.Google ScholarCross Ref
- Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2018. An AssertionBased Program Logic for Probabilistic Programs. In European Symposium on Programming (ESOP), Thessaloniki, Greece. arXiv: cs.LO/1803.05535 https://arxiv.org/abs/1803.05535Google Scholar
- Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2016b. A Program Logic for Union Bounds. In International Colloquium on Automata, Languages and Programming (ICALP), Rome, Italy. 107:1–107:15.Google Scholar
- Vaishak Belle, Andrea Passerini, and Guy Van den Broeck. 2015. Probabilistic Inference in Hybrid Domains by Weighted Model Integration. In International Joint Conference on Artificial Intelligence (IJCAI), Buenos Aires, Argentina. 2770–2776. http://ijcai.org/Abstract/15/392 Google ScholarDigital Library
- Olivier Bousquet and André Elisseeff. 2002. Stability and generalization. Journal of Machine Learning Research 2, Mar (2002), 499–526. https://www.jmlr.org/papers/v2/bousquet02a.html Google ScholarDigital Library
- Michael Carbin, Sasa Misailovic, and Martin C Rinard. 2013. Verifying quantitative reliability for programs that execute on unreliable hardware. In ACM SIGPLAN Conference on Object Oriented Programming: Systems, Languages, and Applications (OOPSLA), Indianapolis, Indiana, Vol. 48. 33–52. Google ScholarDigital Library
- Rohit Chadha, Luís Cruz-Filipe, Paulo Mateus, and Amílcar Sernadas. 2007. Reasoning about probabilistic sequential programs. Theoretical Computer Science 379, 1 (2007), 142–165. Google ScholarDigital Library
- Aleksandar Chakarov and Sriram Sankaranarayanan. 2013. Probabilistic program analysis with martingales. In International Conference on Computer Aided Verification (CAV), Saint Petersburg, Russia. 511–526. https://www.cs.colorado.edu/ ~srirams/papers/cav2013- martingales.pdfGoogle ScholarCross Ref
- T.-H. Hubert Chan, Elaine Shi, and Dawn Song. 2011. Private and continual release of statistics. ACM Transactions on Information and System Security 14, 3 (2011), 26. https://eprint.iacr.org/2010/076.pdf Google ScholarDigital Library
- Krishnendu Chatterjee, Hongfei Fu, and Amir Kafshdar Goharshady. 2016a. Termination Analysis of Probabilistic Programs through Positivstellensatz’s. In International Conference on Computer Aided Verification (CAV), Toronto, Ontario (Lecture Notes in Computer Science), Vol. 9779. Springer-Verlag, 3–22.Google ScholarCross Ref
- Krishnendu Chatterjee, Hongfei Fu, Petr Novotný, and Rouzbeh Hasheminezhad. 2016b. Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs. In ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), Saint Petersburg, Florida. 327–342. Google ScholarDigital Library
- Krishnendu Chatterjee, Petr Novotný, and Ðorđe Žikelić. 2017. Stochastic Invariants for Probabilistic Termination. In ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), Paris, France. 145–160. Google ScholarDigital Library
- Dmitry Chistikov, Rayna Dimitrova, and Rupak Majumdar. 2015. Approximate Counting in SMT and Value Estimation for Probabilistic Programs. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), London, England. 320–334. Google ScholarDigital Library
- Jürgen Christ and Jochen Hoenicke. 2016. Proof Tree Preserving Tree Interpolation. J. Autom. Reasoning 57, 1 (2016), 67–95. Google ScholarDigital Library
- Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, and Roberto Sebastiani. 2013. The MathSAT5 SMT solver. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Rome, Italy. Springer, 93–107. Google ScholarDigital Library
- Guillaume Claret, Sriram K. Rajamani, Aditya V. Nori, Andrew D. Gordon, and Johannes Borgström. 2013. Bayesian inference using data flow analysis. In Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE), Saint Petersburg, Russia. 92–102. Google ScholarDigital Library
- Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2005. Abstraction refinement for termination. In International Symposium on Static Analysis (SAS), London, England. Springer-Verlag, 87–101. Google ScholarDigital Library
- Patrick Cousot and Michael Monerau. 2012. Probabilistic abstract interpretation. In European Symposium on Programming (ESOP), Tallinn, Estonia. Springer-Verlag, 169–193. Google ScholarDigital Library
- William Craig. 1957. Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. The Journal of Symbolic Logic 22, 3 (1957), 269–285.Google ScholarCross Ref
- Marco Cusumano-Towner, Benjamin Bichsel, Timon Gehr, Martin Vechev, and Vikash K Mansinghka. 2018. Incremental inference for probabilistic programs. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Philadelphia, Pennsylvania. 571–585. Google ScholarDigital Library
- Leonardo Mendonça de Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Budapest, Hungary. Google ScholarDigital Library
- Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, and Matthias Volk. 2017. A storm is Coming: A Modern Probabilistic Model Checker. In International Conference on Computer Aided Verification (CAV), Heidelberg, Germany (Lecture Notes in Computer Science), Vol. abs/1702.04311. Springer-Verlag. arXiv: 1702.04311 http://arxiv.org/abs/1702.04311Google ScholarCross Ref
- J. den Hartog. 2002. Probabilistic extensions of semantical models. Ph.D. Dissertation. Vrije Universiteit Amsterdam.Google Scholar
- Cynthia Dwork, Moritz Hardt, Toniann Pitassi, Omer Reingold, and Richard Zemel. 2012. Fairness through awareness. In ACM SIGACT Innovations in Theoretical Computer Science (ITCS), Cambridge, Massachusetts. 214–226. Google ScholarDigital Library
- Cynthia Dwork, Frank McSherry, Kobbi Nissim, and Adam D. Smith. 2006. Calibrating Noise to Sensitivity in Private Data Analysis. In IACR Theory of Cryptography Conference (TCC), New York, New York (Lecture Notes in Computer Science), Vol. 3876. Springer-Verlag, 265–284. Google ScholarDigital Library
- Cynthia Dwork, Moni Naor, Toniann Pitassi, and Guy N. Rothblum. 2010. Differential privacy under continual observation. In ACM SIGACT Symposium on Theory of Computing (STOC), Cambridge, Massachusetts. 715–724. https://www.mit.edu/ ~rothblum/papers/continalobs.pdf Google ScholarDigital Library
- Cynthia Dwork and Aaron Roth. 2014. The Algorithmic Foundations of Differential Privacy. Foundations and Trends® in Theoretical Computer Science 9, 3–4 (2014), 211–407. Google ScholarDigital Library
- Azadeh Farzan, Zachary Kincaid, and Andreas Podelski. 2013. Inductive Data Flow Graphs. In ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), Rome, Italy. 129–142. Google ScholarDigital Library
- Timon Gehr, Sasa Misailovic, Petar Tsankov, Laurent Vanbever, Pascal Wiesmann, and Martin Vechev. 2018. Bayonet: probabilistic inference for networks. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Philadelphia, Pennsylvania. 586–602. Google ScholarDigital Library
- Timon Gehr, Sasa Misailovic, and Martin Vechev. 2016. PSI: Exact symbolic inference for probabilistic programs. In International Conference on Computer Aided Verification (CAV), Toronto, Ontario. Springer-Verlag, 62–83.Google ScholarCross Ref
- Susanne Graf and Hassen Saïdi. 1997. Construction of abstract state graphs with PVS. In International Conference on Computer Aided Verification (CAV), Haifa, Israel. Springer-Verlag, 72–83. Google ScholarDigital Library
- Samuel Haney, Ashwin Machanavajjhala, John M Abowd, Matthew Graham, Mark Kutzbach, and Lars Vilhuber. 2017. Utility Cost of Formal Privacy for Releasing National Employer-Employee Statistics. In ACM SIGMOD International Conference on Management of Data (SIGMOD), Chicago, Illinois. 1339–1354. Google ScholarDigital Library
- Matthias Heizmann, Yu-Fang Chen, Daniel Dietsch, Marius Greitschus, Jochen Hoenicke, Yong Li, Alexander Nutz, Betim Musa, Christian Schilling, Tanja Schindler, and Andreas Podelski. 2018. Ultimate Automizer and the Search for Perfect Interpolants (Competition Contribution). In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Thessaloniki, Greece. 447–451.Google Scholar
- Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. 2009. Refinement of trace abstraction. In International Symposium on Static Analysis (SAS), Los Angeles, California. Springer-Verlag, 69–85. Google ScholarDigital Library
- Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. 2010. Nested Interpolants. In ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), Madrid, Spain. 471–482. Google ScholarDigital Library
- Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. 2013. Software model checking for people who love automata. In International Conference on Computer Aided Verification (CAV), Saint Petersburg, Russia. Springer-Verlag, 36–52.Google ScholarCross Ref
- Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Kenneth L. McMillan. 2004. Abstractions from proofs. In ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), Venice, Italy, Vol. 39. 232–244. Google ScholarDigital Library
- Holger Hermanns, Björn Wachter, and Lijun Zhang. 2008. Probabilistic CEGAR. In International Conference on Computer Aided Verification (CAV), Princeton, New Jersey. Springer-Verlag, 162–175. Google ScholarDigital Library
- Jochen Hoenicke and Tanja Schindler. 2018. Efficient Interpolation for the Theory of Arrays. In International Joint Conference on Artificial Intelligence (IJCAI), Oxford, England (Lecture Notes in Computer Science), Vol. 10900. Springer-Verlag, 549–565.Google Scholar
- Noah Johnson, Joseph P Near, and Dawn Song. 2018. Towards practical differential privacy for SQL queries. Proceedings of the VLDB Endowment 11, 5 (2018), 526–539. Appeared at the International Conference on Very Large Data Bases (VLDB), Rio de Janeiro, Brazil. Google ScholarDigital Library
- Joost-Pieter Katoen. 2016. The Probabilistic Model Checking Landscape. In IEEE Symposium on Logic in Computer Science (LICS), New York, New York. 31–45. Google ScholarDigital Library
- Mark Kattenbelt, Marta Kwiatkowska, Gethin Norman, and David Parker. 2009. Abstraction Refinement for Probabilistic Software. In International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), Savannah, Georgia. Springer-Verlag, 182–197. Google ScholarDigital Library
- Mark Kattenbelt, Marta Kwiatkowska, Gethin Norman, and David Parker. 2010. A game-based abstraction-refinement framework for Markov decision processes. Formal Methods in System Design 36, 3 (01 Sep 2010), 246–280. Google ScholarDigital Library
- Dexter Kozen. 1985. A Probabilistic PDL. J. Comput. System Sci. 30, 2 (1985).Google ScholarCross Ref
- Marta Kwiatkowska, Gethin Norman, and David Parker. 2010. Advances and challenges of probabilistic model checking. In Annual Allerton Conference on Communication, Control, and Computing (Allerton). IEEE, 1691–1698.Google ScholarCross Ref
- Marta Kwiatkowska, Gethin Norman, and David Parker. 2011. PRISM 4.0: Verification of probabilistic real-time systems. In International Conference on Computer Aided Verification (CAV), Snowbird, Utah (Lecture Notes in Computer Science), Vol. 6806. Springer-Verlag, 585–591. Google ScholarDigital Library
- Michael L. Littman, Stephen M Majercik, and Toniann Pitassi. 2001. Stochastic Boolean satisfiability. Journal of Automated Reasoning 27, 3 (2001), 251–296. Google ScholarDigital Library
- Piotr Mardziel, Stephen Magill, Michael Hicks, and Mudhakar Srivatsa. 2011. Dynamic enforcement of knowledge-based security policies. In IEEE Computer Security Foundations Symposium (CSF), Domaine de l’Abbaye des Vaux de Cernay, France. 114–128. Google ScholarDigital Library
- Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, and Joost-Pieter Katoen. 2018. A new proof rule for almost-sure termination. Proceedings of the ACM on Programming Languages 2, POPL (2018), 33:1–33:28. Google ScholarDigital Library
- Kenneth L. McMillan. 2003. Interpolation and SAT-based model checking. In International Conference on Computer Aided Verification (CAV), Boulder, Colorado. Springer-Verlag, 1–13.Google ScholarCross Ref
- Kenneth L. McMillan. 2006. Lazy abstraction with interpolants. In International Conference on Computer Aided Verification (CAV), Seattle, Washington. Springer-Verlag, 123–136. Google ScholarDigital Library
- Frank McSherry and Kunal Talwar. 2007. Mechanism Design via Differential Privacy. In IEEE Symposium on Foundations of Computer Science (FOCS), Providence, Rhode Island. 94–103. Google ScholarDigital Library
- David Monniaux. 2000. Abstract interpretation of probabilistic semantics. In International Symposium on Static Analysis (SAS), Santa Barbara, California. Springer-Verlag, 322–339. Google ScholarDigital Library
- David Monniaux. 2001. Backwards abstract interpretation of probabilistic programs. In European Symposium on Programming (ESOP), Genova, Italy. Springer-Verlag, 367–382. Google ScholarDigital Library
- David Monniaux. 2005. Abstract interpretation of programs as Markov decision processes. Science of Computer Programming 58, 1 (2005), 179–205. Google ScholarDigital Library
- Carroll Morgan, Annabelle McIver, and Karen Seidel. 1996. Probabilistic Predicate Transformers. ACM Transactions on Programming Languages and Systems 18, 3 (1996), 325–353. Google ScholarDigital Library
- Praveen Narayanan, Jacques Carette, Wren Romano, Chung-chieh Shan, and Robert Zinkov. 2016. Probabilistic inference by program transformation in Hakaru (system description). In International Symposium on Functional and Logic Programming (FLOPS), Kochi, Japan. Springer-Verlag, 62–79.Google ScholarCross Ref
- Robert Rand and Steve Zdancewic. 2015. VPHL: A Verified Partial-Correctness Logic for Probabilistic Programs. In Conference on the Mathematical Foundations of Programming Semantics (MFPS), Nijmegen, The Netherlands.Google Scholar
- Philipp Rümmer, Hossein Hojjat, and Viktor Kuncak. 2013. Classifying and solving Horn clauses for verification. In Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Menlo Park, California. Springer, 1–21. Google ScholarDigital Library
- Philipp Rummer and Pavle Subotic. 2013. Exploring interpolants. In Formal Methods in Computer-Aided Design (FMCAD), Portland, Oregon. IEEE, 69–76.Google Scholar
- C. Smith, J. Hsu, and A. Albarghouthi. 2018. Trace Abstraction Modulo Probability. ArXiv e-prints (Oct. 2018). arXiv: cs.PL/1810.12396Google Scholar
- Akhilesh Srikanth, Burak Sahin, and William R. Harris. 2017. Complexity Verification Using Guided Theorem Enumeration. In ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), Paris, France. 639–652. Google ScholarDigital Library
- Tino Teige and Martin Fränzle. 2011. Generalized Craig interpolation for stochastic Boolean satisfiability problems. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Saarbrücken, Germany. Springer-Verlag, 158–172. Google ScholarDigital Library
- Di Wang, Jan Hoffmann, and Thomas Reps. 2018. PMAF: An Algebraic Framework for Static Analysis of Probabilistic Programs. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Philadelphia, Pennsylvania. Google ScholarDigital Library
- Stanley L. Warner. 1965. Randomized response: A survey technique for eliminating evasive answer bias. J. Amer. Statist. Assoc. 60, 309 (1965), 63–69.Google ScholarCross Ref
Index Terms
- Trace abstraction modulo probability
Recommendations
Trace Abstraction-Based Verification for Uninterpreted Programs
Formal MethodsAbstractThe verification of uninterpreted programs is undecidable in general. This paper proposes to employ counterexample-guided abstraction refinement (CEGAR) framework for verifying uninterpreted programs. Different from the existing interpolant-based ...
SAT-based Abstraction Refinement for Real-time Systems
In this paper, we present an abstraction refinement approach for model checking safety properties of real-time systems using SAT-solving. We present a faithful embedding of bounded model checking for systems of timed automata into propositional logic ...
Slicing Abstractions
Fundamentals of Software Engineering 2007: Selected ContributionsAbstraction and slicing are both techniques for reducing the size of the state space to be inspected during verification. In this paper, we present a new model checking procedure for infinite-state concurrent systems that interleaves automatic ...
Comments