Azadeh Farzan
Skip Abstract Section
Skip Supplemental Material SectionAbstract
Program reductions are used widely to simplify reasoning about the correctness of concurrent and distributed programs. In this paper, we propose a general approach to proof simplification of concurrent programs based on exploring generic classes of reductions. We introduce two classes of sound program reductions, study their theoretical properties, show how they can be effectively used in algorithmic verification, and demonstrate that they are very effective in producing proofs of a diverse class of programs without targeting specific syntactic properties of these programs. The most novel contribution of this paper is the introduction of the concept of context in the definition of program reductions. We demonstrate how commutativity of program steps in some program contexts can be used to define a generic class of sound reductions which can be used to automatically produce proofs for programs whose complete Floyd-Hoare style proofs are theoretically beyond the reach of automated verification technology of today.
Supplemental Material
- Parosh Aziz Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos Sagonas. 2014. Optimal dynamic partial order reduction. In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014, Suresh Jagannathan and Peter Sewell (Eds.). ACM, 373–384.Google Scholar
Digital Library
- Parosh Aziz Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos Sagonas. 2017. Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction. J. ACM 64, 4 (2017), 25:1–25:49.Google ScholarDigital Library
- Franz Baader and Stephan Tobies. 2001. The Inverse Method Implements the Automata Approach for Modal Satisfiability. In Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 18-23, 2001, Proceedings (Lecture Notes in Computer Science), Rajeev Goré, Alexander Leitsch, and Tobias Nipkow (Eds.), Vol. 2083. Springer, 92–106.Google Scholar
- Gilles Barthe, Juan Manuel Crespo, and César Kunz. 2011. Relational Verification Using Product Programs. In FM 2011: Formal Methods - 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011. Proceedings (Lecture Notes in Computer Science), Michael J. Butler and Wolfram Schulte (Eds.), Vol. 6664. Springer, 200–214.Google ScholarDigital Library
- Mikolaj Bojanczyk, Bartek Klin, and Slawomir Lasota. 2014. Automata theory in nominal sets. Logical Methods in Computer Science 10, 3 (2014).Google Scholar
- Franck Cassez and Frowin Ziegler. 2015. Verification of Concurrent Programs Using Trace Abstraction Refinement. In Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings (Lecture Notes in Computer Science), Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov (Eds.), Vol. 9450. Springer, 233–248.Google ScholarDigital Library
- Ankush Desai, Pranav Garg, and P. Madhusudan. 2014. Natural proofs for asynchronous programs using almost-synchronous reductions. In Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2014, part of SPLASH 2014, Portland, OR, USA, October 20-24, 2014, Andrew P. Black and Todd D. Millstein (Eds.). ACM, 709–725.Google Scholar
- Volker Diekert and Yves Métivier. 1997. Partial Commutation and Traces. In Handbook of Formal Languages, Volume 3: Beyond Words., Grzegorz Rozenberg and Arto Salomaa (Eds.). Springer, 457–533.Google Scholar
- Volker Diekert and Grzegorz Rozenberg (Eds.). 1995. The Book of Traces. World Scientific.Google Scholar
- Tayfun Elmas, Shaz Qadeer, and Serdar Tasiran. 2009. A calculus of atomic actions. In Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009, Zhong Shao and Benjamin C. Pierce (Eds.). ACM, 2–15.Google ScholarDigital Library
- Azadeh Farzan, Zachary Kincaid, and Andreas Podelski. 2013. Inductive data flow graphs. In The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’13, Rome, Italy - January 23 - 25, 2013, Roberto Giacobazzi and Radhia Cousot (Eds.). ACM, 129–142.Google ScholarDigital Library
- Azadeh Farzan, Zachary Kincaid, and Andreas Podelski. 2015. Proof Spaces for Unbounded Parallelism. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, Sriram K. Rajamani and David Walker (Eds.). ACM, 407–420.Google ScholarDigital Library
- Azadeh Farzan and Anthony Vandikas. 2019a. Automated Hypersafety Verification. In Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I (Lecture Notes in Computer Science), Isil Dillig and Serdar Tasiran (Eds.), Vol. 11561. Springer, 200–218.Google Scholar
- Azadeh Farzan and Anthony Vandikas. 2019b. Reductions for Safety Proofs (Extended Version). CoRR abs/1910.14619 (2019). arXiv: 1910.14619 http://arxiv.org/abs/1910.14619Google Scholar
- Cormac Flanagan, Stephen N. Freund, and Shaz Qadeer. 2005. Exploiting Purity for Atomicity. IEEE Trans. Software Eng. 31, 4 (2005), 275–291.Google ScholarDigital Library
- Cormac Flanagan and Shaz Qadeer. 2003. A type and effect system for atomicity. In Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation 2003, San Diego, California, USA, June 9-11, 2003, Ron Cytron and Rajiv Gupta (Eds.). ACM, 338–349.Google ScholarDigital Library
- Blaise Genest, Dietrich Kuske, and Anca Muscholl. 2007. On Communicating Automata with Bounded Channels. Fundam. Inform. 80, 1-3 (2007), 147–167.Google Scholar
- Patrice Godefroid. 1996. Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem. Lecture Notes in Computer Science, Vol. 1032. Springer.Google ScholarDigital Library
- Patrice Godefroid and Didier Pirottin. 1993. Refining Dependencies Improves Partial-Order Verification Methods (Extended Abstract). In Computer Aided Verification, 5th International Conference, CAV ’93, Elounda, Greece, June 28 - July 1, 1993, Proceedings (Lecture Notes in Computer Science), Costas Courcoubetis (Ed.), Vol. 697. Springer, 438–449.Google Scholar
- Joseph A. Goguen and José Meseguer. 1982. Security Policies and Security Models. In 1982 IEEE Symposium on Security and Privacy, Oakland, CA, USA, April 26-28, 1982. IEEE Computer Society, 11–20.Google Scholar
- Chris Hawblitzel, Erez Petrank, Shaz Qadeer, and Serdar Tasiran. 2015. Automated and Modular Refinement Reasoning for Concurrent Programs. In Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II (Lecture Notes in Computer Science), Daniel Kroening and Corina S. Pasareanu (Eds.), Vol. 9207. Springer, 449–465.Google Scholar
- Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. 2009. Refinement of Trace Abstraction. In Static Analysis, 16th International Symposium, SAS 2009, Los Angeles, CA, USA, August 9-11, 2009. Proceedings (Lecture Notes in Computer Science), Jens Palsberg and Zhendong Su (Eds.), Vol. 5673. Springer, 69–85.Google Scholar
- Shmuel Katz and Doron A. Peled. 1992. Defining Conditional Independence Using Collapses. Theor. Comput. Sci. 101, 2 (1992), 337–359.Google ScholarDigital Library
- Bernhard Kragl, Shaz Qadeer, and Thomas A. Henzinger. 2018. Synchronizing the Asynchronous. In 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China (LIPIcs), Sven Schewe and Lijun Zhang (Eds.), Vol. 118. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 21:1–21:17.Google Scholar
- Richard J. Lipton. 1975. Reduction: A Method of Proving Properties of Parallel Programs. Commun. ACM 18, 12 (1975), 717–721.Google ScholarDigital Library
- Amir Pnueli, Michael Siegel, and Eli Singerman. 1998. Translation Validation. In Tools and Algorithms for Construction and Analysis of Systems, 4th International Conference, TACAS ’98, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS’98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings (Lecture Notes in Computer Science), Bernhard Steffen (Ed.), Vol. 1384. Springer, 151–166.Google Scholar
- Andrei Sabelfeld and Andrew C. Myers. 2003. Language-based information-flow security. IEEE Journal on Selected Areas in Communications 21, 1 (2003), 5–19.Google ScholarDigital Library
- Vladimiro Sassone, Mogens Nielsen, and Glynn Winskel. 1993. Deterministic Behavioural Models for Concurrency. In Mathematical Foundations of Computer Science 1993, 18th International Symposium, MFCS’93, Gdansk, Poland, August 30 -September 3, 1993, Proceedings (Lecture Notes in Computer Science), Andrzej M. Borzyszkowski and Stefan Sokolowski (Eds.), Vol. 711. Springer, 682–692.Google Scholar
- Marcelo Sousa and Isil Dillig. 2016. Cartesian hoare logic for verifying k-safety properties. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016, Chandra Krintz and Emery Berger (Eds.). ACM, 57–69.Google ScholarDigital Library
- Marcelo Sousa, Isil Dillig, Dimitrios Vytiniotis, Thomas Dillig, and Christos Gkantsidis. 2014. Consolidation of queries with user-defined functions. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’14, Edinburgh, United Kingdom - June 09 - 11, 2014, Michael F. P. O’Boyle and Keshav Pingali (Eds.). ACM, 554–564.Google ScholarDigital Library
- Klaus von Gleissenthall, Rami Gökhan Kici, Alexander Bakst, Deian Stefan, and Ranjit Jhala. 2019. Pretend synchrony: synchronous verification of asynchronous distributed programs. PACMPL 3, POPL (2019), 59:1–59:30.Google Scholar
- Björn Wachter, Daniel Kroening, and Joël Ouaknine. 2013. Verifying multi-threaded software with impact. In Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013. IEEE, 210–217.Google Scholar
- Chao Wang, Swarat Chaudhuri, Aarti Gupta, and Yu Yang. 2009. Symbolic pruning of concurrent program executions. In Proceedings of the 7th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2009, Amsterdam, The Netherlands, August 24-28, 2009, Hans van Vliet and Valérie Issarny (Eds.). ACM, 23–32.Google ScholarDigital Library
- Chao Wang, Zijiang Yang, Vineet Kahlon, and Aarti Gupta. 2008. Peephole Partial Order Reduction. In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings (Lecture Notes in Computer Science), C. R. Ramakrishnan and Jakob Rehof (Eds.), Vol. 4963. Springer, 382–396.Google ScholarCross Ref
- Martin De Wulf, Laurent Doyen, Thomas A. Henzinger, and Jean-François Raskin. 2006. Antichains: A New Algorithm for Checking Universality of Finite Automata. In Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings (Lecture Notes in Computer Science), Thomas Ball and Robert B. Jones (Eds.), Vol. 4144. Springer, 17–30.Google Scholar
Index Terms
- Reductions for safety proofs
Recommendations
Natural proofs for asynchronous programs using almost-synchronous reductions
OOPSLA '14We consider the problem of provably verifying that an asynchronous message-passing system satisfies its local assertions. We present a novel reduction scheme for asynchronous event-driven programs that finds almost-synchronous invariants - invariants ...
Natural proofs for asynchronous programs using almost-synchronous reductions
OOPSLA '14: Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & ApplicationsWe consider the problem of provably verifying that an asynchronous message-passing system satisfies its local assertions. We present a novel reduction scheme for asynchronous event-driven programs that finds almost-synchronous invariants - invariants ...
Proof Spaces for Unbounded Parallelism
POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming LanguagesIn this paper, we present a new approach to automatically verify multi-threaded programs which are executed by an unbounded number of threads running in parallel.
The starting point for our work is the problem of how we can leverage existing automated ...
Comments