Document Open Access Logo

A New Notion of Compositionality for Concurrent Program Proofs (Invited Talk)

Authors Azadeh Farzan, Zachary Kincaid

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2017.4.pdf
  • Filesize: 0.68 MB
  • 11 pages

Document Identifiers

Author Details

Azadeh Farzan
Zachary Kincaid

Cite As Get BibTex

Azadeh Farzan and Zachary Kincaid. A New Notion of Compositionality for Concurrent Program Proofs (Invited Talk). In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 4:1-4:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.CONCUR.2017.4

Abstract

This paper presents a high level overview of Proof Spaces [Farzan, Kincaid, and Podelski, 2015] as an instance of a new approach to compositional verification of concurrent programs and discusses potential future work extending the approach beyond its current scope of applicability.

Subject Classification

Keywords
  • Concurrency
  • Proofs
  • Dynamic Memory
  • Recursion

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Aws Albarghouthi, Josh Berdine, Byron Cook, and Zachary Kincaid. Spatial interpolants. In Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, pages 634-660, 2015. Google Scholar
  2. Aws Albarghouthi and Kenneth L. McMillan. Beautiful interpolants. In CAV, pages 313-329, 2013. Google Scholar
  3. Stephen Brookes and Peter W. O'Hearn. Concurrent separation logic. SIGLOG News, 3(3):47-65, 2016. Google Scholar
  4. Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, and L. J. Hwang. Symbolic model checking: 10^20 states and beyond. In Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS '90), Philadelphia, Pennsylvania, USA, June 4-7, 1990, pages 428-439, 1990. Google Scholar
  5. Michael Colón, Sriram Sankaranarayanan, and Henny Sipma. Linear invariant generation using non-linear constraint solving. In CAV, pages 420-432, 2003. Google Scholar
  6. Patrick Cousot and Radhia Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL, pages 238-252, 1977. Google Scholar
  7. Patrick Cousot and Nicolas Halbwachs. Automatic discovery of linear restraints among variables of a program. In POPL, pages 84-96, 1978. Google Scholar
  8. Thomas Dinsdale-Young, Pedro da Rocha Pinto, Kristoffer Just Andersen, and Lars Birkedal. Caper - automatic verification for fine-grained concurrency. In Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, pages 420-447, 2017. Google Scholar
  9. Azadeh Farzan, Zachary Kincaid, and Andreas Podelski. 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, pages 129-142, 2013. Google Scholar
  10. Azadeh Farzan, Zachary Kincaid, and Andreas Podelski. Proofs that count. In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014, pages 151-164, 2014. Google Scholar
  11. Azadeh Farzan, Zachary Kincaid, and Andreas Podelski. 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, pages 407-420, 2015. Google Scholar
  12. Azadeh Farzan, Zachary Kincaid, and Andreas Podelski. Proving liveness of parameterized programs. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 185-196, 2016. Google Scholar
  13. Patrice Godefroid. Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem. PhD thesis, University of Liege, 1994. Google Scholar
  14. Ashutosh Gupta, Rupak Majumdar, and Andrey Rybalchenko. From tests to proofs. In TACAS, pages 262-276, 2009. Google Scholar
  15. Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Kenneth L. McMillan. Abstractions from proofs. In POPL, pages 232-244, 2004. Google Scholar
  16. Cliff B. Jones. Specification and design of (parallel) programs. In IFIP Congress, pages 321-332, 1983. Google Scholar
  17. Kenneth L. McMillan. Symbolic model checking. Kluwer, 1993. Google Scholar
  18. Kenneth. L. McMillan. Lazy abstraction with interpolants. In CAV, pages 123-136, 2006. Google Scholar
  19. Peter W. O'Hearn. Resources, concurrency and local reasoning. In CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings, pages 49-67, 2004. Google Scholar
  20. Peter W. O'Hearn. Resources, concurrency, and local reasoning. Theor. Comput. Sci., 375(1-3):271-307, 2007. Google Scholar
  21. Peter W. O'Hearn, John C. Reynolds, and Hongseok Yang. Local reasoning about programs that alter data structures. In Computer Science Logic, 15th International Workshop, CSL 2001. 10th Annual Conference of the EACSL, Paris, France, September 10-13, 2001, Proceedings, pages 1-19, 2001. Google Scholar
  22. Susan Owicki and David Gries. Verifying properties of parallel programs: an axiomatic approach. CACM, 19:279-285, May 1976. Google Scholar
  23. Doron Peled. All from one, one for all: On model checking using representatives. In CAV, pages 409-423, 1993. Google Scholar
  24. Shaz Qadeer, Sriram K. Rajamani, and Jakob Rehof. Summarizing procedures in concurrent programs. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14-16, 2004, pages 245-255, 2004. Google Scholar
  25. G. Ramalingam. Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Program. Lang. Syst., 22(2):416-430, March 2000. Google Scholar
  26. John C. Reynolds. Separation logic: A logic for shared mutable data structures. In 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings, pages 55-74, 2002. Google Scholar
  27. Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. Mechanized verification of fine-grained concurrent programs. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015, pages 77-87, 2015. Google Scholar
  28. Micha Sharir and Amir Pnueli. Two Approaches to Interprocedural Data Flow Analysis, chapter 7. Prentice-Hall, Inc., 1981. Google Scholar
  29. R. Treiber. Systems programming: coping with parallelism. Technical report, Almaden Research Center, 1986. Google Scholar
  30. Aaron Turon, Derek Dreyer, and Lars Birkedal. Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency. In ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA - September 25 - 27, 2013, pages 377-390, 2013. Google Scholar
  31. Viktor Vafeiadis. Rgsep action inference. In Proceedings of the 11th International Conference on Verification, Model Checking, and Abstract Interpretation, pages 345-361, 2010. Google Scholar
  32. Antti Valmari. Stubborn sets for reduced state space generation. In Advances in Petri Nets, pages 491-515, 1991. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact