research-article

Open access

Igloo: soundly linking compositional refinement and separation logic for distributed system verification

Authors:

Christoph Sprenger,

Martin Clochard,

David BasinAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 4, Issue OOPSLA

Article No.: 152, Pages 1 - 31

https://doi.org/10.1145/3428220

Published: 13 November 2020 Publication History

Abstract

Lighthouse projects like CompCert, seL4, IronFleet, and DeepSpec have demonstrated that full system verification is feasible by establishing a refinement between an abstract system specification and an executable implementation. Existing approaches however impose severe restrictions on the abstract system specifications due to their limited expressiveness or versatility, or on the executable code due to their use of suboptimal code extraction or inexpressive program logics. We propose a novel methodology that combines the compositional refinement of event-based models of distributed systems with the verification of full-fledged program code using expressive separation logics, which support features of realistic programming languages like heap data structures and concurrency. Our main technical contribution is a formal framework that soundly relates event-based system models to program specifications in separation logics. This enables protocol development tools to soundly interoperate with program verifiers to establish a refinement between the model and the code. We formalized our framework, Igloo, in Isabelle/HOL. We report on three case studies, a leader election protocol, a replication protocol, and a security protocol, for which we refine formal requirements into program specifications that we implement in Java and Python and prove correct using the VeriFast and Nagini tools.

Supplementary Material

Auxiliary Presentation Video (oopsla20main-p95-p-video.mp4)

OOPSLA 2020 talk given on Nov 20+21.

Download
37.77 MB

References

[1]

Martín Abadi and Leslie Lamport. 1991. The Existence of Refinement Mappings. Theor. Comput. Sci. 82, 2 ( 1991 ), 253-284. https://doi.org/10.1016/ 0304-3975 ( 91 ) 90224-P

Digital Library

[2]

Jean-Raymond Abrial. 2010. Modeling in Event-B-System and Software Engineering. Cambridge University Press. https: //doi.org/10.1017/CBO9781139195881

[3]

Andrew W. Appel. 2012. Verified Software Toolchain. In NASA Formal Methods-4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings. 2. https://doi.org/10.1007/978-3-642-28891-3_2

Digital Library

[4]

Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, and Dmitriy Traytel. 2017. Friends with Benefits-Implementing Corecursion in Foundational Proof Assistants. 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 (Lecture Notes in Computer Science, Vol. 10201 ), Hongseok Yang (Ed.). Springer, 111-140. https://doi.org/10.1007/978-3-662-54434-1_5

Digital Library

[5]

Christian Cachin, Rachid Guerraoui, and Luís E. T. Rodrigues. 2011. Introduction to Reliable and Secure Distributed Programming (2. ed.). Springer. https://doi.org/10.1007/978-3-642-15260-3

[6]

Qinxiang Cao, Lennart Beringer, Samuel Gruetter, Josiah Dodds, and Andrew W. Appel. 2018. VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs. J. Autom. Reasoning 61, 1-4 ( 2018 ), 367-422. https://doi.org/10.1007/s10817-018-9457-5

Digital Library

[7]

Ernest J. H. Chang and Rosemary Roberts. 1979. An Improved Algorithm for Decentralized Extrema-Finding in Circular Configurations of Processes. Commun. ACM 22, 5 ( 1979 ), 281-283. https://doi.org/10.1145/359104.359108

Digital Library

[8]

Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and Carolyn L. Talcott (Eds.). 2007. All About Maude-A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic. Lecture Notes in Computer Science, Vol. 4350. Springer. https://doi.org/10.1007/978-3-540-71999-1

[9]

Sjoerd Cranen, Jan Friso Groote, Jeroen J. A. Keiren, Frank P. M. Stappers, Erik P. de Vink, Wieger Wesselink, and Tim A. C. Willemse. 2013. An Overview of the mCRL2 Toolset and Its Recent Advances. In Tools and Algorithms for the Construction and Analysis of Systems-19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings (Lecture Notes in Computer Science, Vol. 7795 ), Nir Piterman and Scott A. Smolka (Eds.). Springer, 199-213. https://doi.org/10.1007/978-3-642-36742-7_15

Digital Library

[10]

Leonardo Mendonça de Moura and Nikolaj Bjørner. 2008. Z3: An Eficient SMT Solver. 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, Vol. 4963 ), C. R. Ramakrishnan and Jakob Rehof (Eds.). Springer, 337-340. https: //doi.org/10.1007/978-3-540-78800-3_24

[11]

Danny Dolev and Andrew Chi-Chih Yao. 1983. On the security of public key protocols. IEEE Trans. Information Theory 29, 2 ( 1983 ), 198-207. https://doi.org/10.1109/TIT. 1983.1056650

Digital Library

[12]

Cezara Dragoi, Thomas A. Henzinger, and Damien Zuferey. 2016. PSync: a partially synchronous language for fault-tolerant distributed algorithms. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20-22, 2016, Rastislav Bodík and Rupak Majumdar (Eds.). ACM, 400-415. https://doi.org/10.1145/2837614.2837650

Digital Library

[13]

Marco Eilers and Peter Müller. 2018. Nagini: A Static Verifier for Python. In Computer Aided Verification-30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I (Lecture Notes in Computer Science, Vol. 10981 ), Hana Chockler and Georg Weissenbacher (Eds.). Springer, 596-603. https://doi.org/10.1007/978-3-319-96145-3_33

[14]

Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath T. V. Setty, and Brian Zill. 2015. IronFleet: proving practical distributed systems correct. In Proceedings of the 25th Symposium on Operating Systems Principles, SOSP 2015, Monterey, CA, USA, October 4-7, 2015, Ethan L. Miller and Steven Hand (Eds.). ACM, 1-17. https://doi.org/10.1145/2815400.2815428

Digital Library

[15]

Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, and Brian Zill. 2014. Ironclad Apps: End-to-End Security via Automated Full-System Verification. In Operating Systems Design and Implementation (OSDI), Jason Flinn and Hank Levy (Eds.). USENIX Association, 165-181.

[16]

C. A. R. Hoare. 2003. The Verifying Compiler: A Grand Challange for Computing Research. In Modular Programming Languages, Joint Modular Languages Conference, JMLC 2003, Klagenfurt, Austria, August 25-27, 2003, Proceedings (Lecture Notes in Computer Science, Vol. 2789 ), László Böszörményi and Peter Schojer (Eds.). Springer, 25-35. https://doi.org/10. 1007/978-3-540-45213-3_4

[17]

Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, and Frank Piessens. 2011. VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java. In NASA Formal Methods-Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings (Lecture Notes in Computer Science, Vol. 6617 ), Mihaela Gheorghiu Bobaru, Klaus Havelund, Gerard J. Holzmann, and Rajeev Joshi (Eds.). Springer, 41-55. https://doi.org/10.1007/978-3-642-20398-5_4

[18]

Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. 2009. seL4: formal verification of an OS kernel. In Proceedings of the 22nd ACM Symposium on Operating Systems Principles 2009, SOSP 2009, Big Sky, Montana, USA, October 11-14, 2009, Jeanna Neefe Matthews and Thomas E. Anderson (Eds.). ACM, 207-220. https://doi.org/10.1145/1629575.1629596

Digital Library

[19]

Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic. 2019. From C to interaction trees: specifying, verifying, and testing a networked server. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019, Assia Mahboubi and Magnus O. Myreen (Eds.). ACM, 234-248. https://doi.org/10.1145/3293880.3294106

Digital Library

[20]

Leslie Lamport. 1994. The Temporal Logic of Actions. ACM Trans. Program. Lang. Syst. 16, 3 ( 1994 ), 872-923. https: //doi.org/10.1145/177492.177726

Digital Library

[21]

K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming, Artificial Intelligence, and Reasoning-16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers (Lecture Notes in Computer Science, Vol. 6355 ), Edmund M. Clarke and Andrei Voronkov (Eds.). Springer, 348-370. https://doi.org/10.1007/978-3-642-17511-4_20

[22]

K. Rustan M. Leino and Peter Müller. 2009. A Basis for Verifying Multi-threaded Programs. In Programming Languages and Systems, 18th European Symposium on Programming, ESOP 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings (Lecture Notes in Computer Science, Vol. 5502 ), Giuseppe Castagna (Ed.). Springer, 378-393. https://doi.org/10.1007/978-3-642-00590-9_27

Digital Library

[23]

Xavier Leroy. 2006. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, January 11-13, 2006, J. Gregory Morrisett and Simon L. Peyton Jones (Eds.). ACM, 42-54. https://doi.org/10.1145/1111037.1111042

Digital Library

[24]

Mohsen Lesani, Christian J. Bell, and Adam Chlipala. 2016. Chapar: certified causally consistent distributed key-value stores. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20-22, 2016, Rastislav Bodík and Rupak Majumdar (Eds.). ACM, 357-370. https://doi.org/10.1145/2837614.2837622

Digital Library

[25]

Si Liu, Atul Sandur, José Meseguer, Peter Csaba Ölveczky, and Qi Wang. 2020. Generating Correct-by-Construction Distributed Implementations from Formal Maude Designs. In NASA Formal Methods-12th International Symposium, NFM 2020, Mofett Field, CA, USA, May 11-15, 2020, Proceedings (Lecture Notes in Computer Science, Vol. 12229 ), Ritchie Lee, Susmit Jha, and Anastasia Mavridou (Eds.). Springer, 22-40. https://doi.org/10.1007/978-3-030-55754-6_2

[26]

Gavin Lowe. 1997. A Hierarchy of Authentication Specification. In 10th Computer Security Foundations Workshop (CSFW '97), June 10-12, 1997, Rockport, Massachusetts, USA. IEEE Computer Society, 31-44. https://doi.org/10.1109/CSFW. 1997.596782

[27]

Nancy A. Lynch and Frits W. Vaandrager. 1995. Forward and Backward Simulations: I. Untimed Systems. Inf. Comput. 121, 2 ( 1995 ), 214-233. https://doi.org/10.1006/inco. 1995.1134

Digital Library

[28]

William Mansky, Wolf Honoré, and Andrew W. Appel. 2020. Connecting Higher-Order Separation Logic to a FirstOrder Outside World. In Programming Languages and Systems-29th European Symposium on Programming, ESOP 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings (Lecture Notes in Computer Science, Vol. 12075 ), Peter Müller (Ed.). Springer, 428-455. https://doi.org/10.1007/978-3-030-44914-8_16

Digital Library

[29]

Peter Müller, Malte Schwerhof, and Alexander J. Summers. 2016. Viper: A Verification Infrastructure for Permission-Based Reasoning. In Verification, Model Checking, and Abstract Interpretation-17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings. 41-62. https://doi.org/10.1007/978-3-662-49122-5_2

Digital Library

[30]

Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2002. Isabelle/HOL-A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, Vol. 2283. Springer. https://doi.org/10.1007/3-540-45949-9

[31]

Wytse Oortwijn and Marieke Huisman. 2019. Practical Abstractions for Automated Verification of Message Passing Concurrency. In Integrated Formal Methods-15th International Conference, IFM 2019, Bergen, Norway, December 2-6, 2019, Proceedings (Lecture Notes in Computer Science, Vol. 11918 ), Wolfgang Ahrendt and Silvia Lizeth Tapia Tarifa (Eds.). Springer, 399-417. https://doi.org/10.1007/978-3-030-34968-4_22

[32]

Matthew J. Parkinson and Gavin M. Bierman. 2005. Separation logic and abstraction. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005, Jens Palsberg and Martín Abadi (Eds.). ACM, 247-258. https://doi.org/10.1145/1040305.1040326

Digital Library

[33]

Willem Penninckx, Bart Jacobs, and Frank Piessens. 2015. Sound, Modular and Compositional Verification of the Input/Output Behavior of Programs. 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 (Lecture Notes in Computer Science, Vol. 9032 ), Jan Vitek (Ed.). Springer, 158-182. https://doi.org/10.1007/978-3-662-46669-8_7

[34]

Adrian Perrig, Pawel Szalachowski, Raphael M. Reischuk, and Laurent Chuat. 2017. SCION: A Secure Internet Architecture. Springer. https://doi.org/10.1007/978-3-319-67080-5

[35]

Benjamin C. Pierce. 2016. The science of deep specification (keynote). In Companion Proceedings of the 2016 ACM SIGPLAN International Conference on Systems, Programming, Languages and Applications: Software for Humanity, SPLASH 2016, Amsterdam, Netherlands, October 30-November 4, 2016, Eelco Visser (Ed.). ACM, 1. https://doi.org/10.1145/2984043. 2998388

Digital Library

[36]

Ruzica Piskac, Thomas Wies, and Damien Zuferey. 2013. Automating Separation Logic Using SMT. In Computer Aided Verification-25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings (Lecture Notes in Computer Science, Vol. 8044 ), Natasha Sharygina and Helmut Veith (Eds.). Springer, 773-789. https://doi.org/10.1007/978-3-642-39799-8_54

[37]

Jonathan Protzenko, Jean Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella Béguelin, Antoine Delignat-Lavaud, Catalin Hritcu, Karthikeyan Bhargavan, Cédric Fournet, and Nikhil Swamy. 2017. Verified low-level programming embedded in F. PACMPL 1, ICFP ( 2017 ), 17 : 1-17 : 29. https://doi.org/10.1145/3110261

Digital Library

[38]

Vincent Rahli, Ivana Vukotic, Marcus Völp, and Paulo Jorge Esteves Veríssimo. 2018. Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq. In Programming Languages and Systems-27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings (Lecture Notes in Computer Science, Vol. 10801 ), Amal Ahmed (Ed.). Springer, 619-650. https://doi.org/10.1007/978-3-319-89884-1_22

[39]

John C. Reynolds. 2002. 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. IEEE Computer Society, 55-74. https://doi.org/10.1109/LICS. 2002.1029817

[40]

Ilya Sergey, James R. Wilcox, and Zachary Tatlock. 2018. Programming and proving with distributed protocols. PACMPL 2, POPL ( 2018 ), 28 : 1-28 : 30. https://doi.org/10.1145/3158116

Digital Library

[41]

Renato Silva and Michael J. Butler. 2010. Shared Event Composition/Decomposition in Event-B. In Formal Methods for Components and Objects-9th International Symposium, FMCO 2010, Graz, Austria, November 29-December 1, 2010. Revised Papers (Lecture Notes in Computer Science, Vol. 6957 ), Bernhard K. Aichernig, Frank S. de Boer, and Marcello M. Bonsangue (Eds.). Springer, 122-141. https://doi.org/10.1007/978-3-642-25271-6_7

Digital Library

[42]

Christoph Sprenger and David A. Basin. 2018. Refining security protocols. Journal of Computer Security 26, 1 ( 2018 ), 71-120. https://doi.org/10.3233/JCS-16814

[43]

Christoph Sprenger, Tobias Klenze, Marco Eilers, Felix A. Wolf, Peter Müller, Martin Clochard, and David Basin. 2020a. Igloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed Systems Verification. CoRR abs/ 2010.04749 ( October 2020 ). arXiv: 2010.04749 http://arxiv.org/abs/ 2010.04749

[44]

Christoph Sprenger, Tobias Klenze, Marco Eilers, Felix A. Wolf, Peter Müller, Martin Clochard, and David Basin. 2020b. Igloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verification (Artifact). https://doi.org/10.5281/zenodo.4039826

Digital Library

[45]

Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean Karim Zinzindohoue, and Santiago Zanella Béguelin. 2016. Dependent types and multi-monadic efects in F ∗. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20-22, 2016, Rastislav Bodík and Rupak Majumdar (Eds.). ACM, 256-270. https://doi.org/10.1145/2837614.2837655

Digital Library

[46]

Robbert van Renesse and Rachid Guerraoui. 2010. Replication Techniques for Availability. In Replication: Theory and Practice (Lecture Notes in Computer Science, Vol. 5959 ), Bernadette Charron-Bost, Fernando Pedone, and André Schiper (Eds.). Springer, 19-40. https://doi.org/10.1007/978-3-642-11294-2_2

[47]

James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas E. Anderson. 2015. Verdi: a framework for implementing and formally verifying distributed systems. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015, David Grove and Steve Blackburn (Eds.). ACM, 357-368. https://doi.org/10.1145/2737924.2737958

Digital Library

[48]

Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst, and Thomas E. Anderson. 2016. Planning for change in a formal verification of the Raft consensus protocol. In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016, Jeremy Avigad and Adam Chlipala (Eds.). ACM, 154-165. https://doi.org/10.1145/2854065.2854081

Digital Library

[49]

Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. 2020. Interaction trees: representing recursive and impure programs in Coq. Proc. ACM Program. Lang. 4, POPL ( 2020 ), 51 : 1-51 : 32. https://doi.org/10.1145/3371119

Digital Library

Cited By

Timany AGregersen SStefanesco LHinrichsen JGondelman LNieto ABirkedal L(2024)Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional RefinementProceedings of the ACM on Programming Languages10.1145/36328518:POPL(241-272)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632851
Ahrendt WErnst GHerber PHuisman MMonti RUlbrich MWeigl A(2024)The VerifyThis Collaborative Long-Term Challenge SeriesTOOLympics Challenge 202310.1007/978-3-031-67695-6_6(160-170)Online publication date: 26-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-67695-6_6
Eilers MSchwerhoff MMüller P(2024)Verification Algorithms for Automated Separation Logic VerifiersComputer Aided Verification10.1007/978-3-031-65627-9_18(362-386)Online publication date: 26-Jul-2024
https://doi.org/10.1007/978-3-031-65627-9_18
Show More Cited By

Index Terms

Igloo: soundly linking compositional refinement and separation logic for distributed system verification

Recommendations

Distributed causal memory: modular specification and verification in higher-order distributed separation logic

We present the first specification and verification of an implementation of a causally-consistent distributed database that supports modular verification of full functional correctness properties of clients and servers. We specify and reason about the ...
Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement

Expressive state-of-the-art separation logics rely on step-indexing to model semantically complex features and to support modular reasoning about imperative higher-order concurrent and distributed programs. Step- indexing comes, however, with an inherent ...
Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols

We present a foundationally verified implementation of a reliable communication library for asynchronous client-server communication, and a stack of formally verified components on top thereof. Our library is implemented in an OCaml-like language on top ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 4, Issue OOPSLA

November 2020

3108 pages

EISSN:2475-1421

DOI:10.1145/3436718

Issue’s Table of Contents

Copyright © 2020 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 13 November 2020

Published in PACMPL Volume 4, Issue OOPSLA

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

11
Total Citations
View Citations
982
Total Downloads

Downloads (Last 12 months)276
Downloads (Last 6 weeks)47

Reflects downloads up to 30 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Timany AGregersen SStefanesco LHinrichsen JGondelman LNieto ABirkedal L(2024)Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional RefinementProceedings of the ACM on Programming Languages10.1145/36328518:POPL(241-272)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632851
Ahrendt WErnst GHerber PHuisman MMonti RUlbrich MWeigl A(2024)The VerifyThis Collaborative Long-Term Challenge SeriesTOOLympics Challenge 202310.1007/978-3-031-67695-6_6(160-170)Online publication date: 26-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-67695-6_6
Eilers MSchwerhoff MMüller P(2024)Verification Algorithms for Automated Separation Logic VerifiersComputer Aided Verification10.1007/978-3-031-65627-9_18(362-386)Online publication date: 26-Jul-2024
https://doi.org/10.1007/978-3-031-65627-9_18
Klenze TSprenger CBasin D(2023)IsaNetJournal of Computer Security10.3233/JCS-22002131:3(217-259)Online publication date: 1-Jan-2023
https://dl.acm.org/doi/10.3233/JCS-220021
Sammler MSpies SSong YD'Osualdo EKrebbers RGarg DDreyer D(2023)DimSum: A Decentralized Approach to Multi-language Semantics and VerificationProceedings of the ACM on Programming Languages10.1145/35712207:POPL(775-805)Online publication date: 9-Jan-2023
https://dl.acm.org/doi/10.1145/3571220
Arquint LWolf FLallemand JSasse RSprenger CWiesner SBasin DMüller P(2023)Sound Verification of Security Protocols: From Design to Interoperable Implementations2023 IEEE Symposium on Security and Privacy (SP)10.1109/SP46215.2023.10179325(1077-1093)Online publication date: May-2023
https://doi.org/10.1109/SP46215.2023.10179325
Ernst GWeigl A(2023)Verify This: Memcached—A Practical Long-Term Challenge for the Integration of Formal MethodsiFM 202310.1007/978-3-031-47705-8_5(82-89)Online publication date: 6-Nov-2023
https://doi.org/10.1007/978-3-031-47705-8_5
Liu S(2022)All in One: Design, Verification, and Implementation of SNOW-optimal Read Atomic TransactionsACM Transactions on Software Engineering and Methodology10.1145/349451731:3(1-44)Online publication date: 7-Mar-2022
https://dl.acm.org/doi/10.1145/3494517
Ernst GKnapp AMurray T(2022)A Hoare Logic with Regular Behavioral SpecificationsLeveraging Applications of Formal Methods, Verification and Validation. Verification Principles10.1007/978-3-031-19849-6_4(45-64)Online publication date: 17-Oct-2022
https://doi.org/10.1007/978-3-031-19849-6_4
He PWestbrook ECarmer BPhifer CRobert VSmeltzer KŞtefănescu ATomb AWick AYacavone MZdancewic S(2021)A type system for extracting functional specifications from memory-safe imperative programsProceedings of the ACM on Programming Languages10.1145/34855125:OOPSLA(1-29)Online publication date: 15-Oct-2021
https://dl.acm.org/doi/10.1145/3485512
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents