Search Results

Documents authored by Krebbers, Robbert

Document
DOI: 10.4230/LIPIcs.ITP.2024.19
Modular Verification of Intrusive List and Tree Data Structures in Separation Logic

Authors: Marc Hermes and Robbert Krebbers

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
Intrusive linked data structures are commonly used in low-level programming languages such as C for efficiency and to enable a form of generic types. Notably, intrusive versions of linked lists and search trees are used in the Linux kernel and the Boost C++ library. These data structures differ from ordinary data structures in the way that nodes contain only the meta data (i.e. pointers to other nodes), but not the data itself. Instead the programmer needs to embed nodes into the data, thereby avoiding pointer indirections, and allowing data to be part of several data structures. In this paper we address the challenge of specifying and verifying intrusive data structures using separation logic. We aim for modular verification, where we first specify and verify the operations on the nodes (without the data) and then use these specifications to verify clients that attach data. We achieve this by employing a representation predicate that separates the data structure’s node structure from the data that is attached to it. We apply our methodology to singly-linked lists - from which we build cyclic and doubly-linked lists - and binary trees - from which we build binary search trees. All verifications are conducted using the Coq proof assistant, making use of the Iris framework for separation logic.
Cite as

Marc Hermes and Robbert Krebbers. Modular Verification of Intrusive List and Tree Data Structures in Separation Logic. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 19:1-19:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{hermes_et_al:LIPIcs.ITP.2024.19,
  author =	{Hermes, Marc and Krebbers, Robbert},
  title =	{{Modular Verification of Intrusive List and Tree Data Structures in Separation Logic}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{19:1--19:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.19},
  URN =		{urn:nbn:de:0030-drops-207478},
  doi =		{10.4230/LIPIcs.ITP.2024.19},
  annote =	{Keywords: Separation Logic, Program Verification, Data Structures, Iris, Coq}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.ITP.2023.2
Interactive and Automated Proofs in Modal Separation Logic (Invited Talk)

Authors: Robbert Krebbers

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract
In program verification, it is common to embed a high-level object logic into the meta logic of a proof assistant to hide low-level aspects of the verification. To verify imperative and concurrent programs, separation logic hides explicit reasoning about heaps and pointer disjointness. To verify programs with cyclic features such as modules or higher-order state, modal logic provides modalities to hide explicit reasoning about step-indices that are used to stratify recursion. The meta logic of proof assistants such as Coq is well suited to embed high-level object logics and prove their soundness. However, proof assistants such as Coq do not have native infrastructure to facilitate proofs in embedded logics - their proof contexts and built-in tactics for interactive and automated proofs are tailored to the connectives of the meta logic, and do not extend to those of the object logic. This results in proofs that are at a too low level of abstraction because they are cluttered with bookkeeping code related to manipulating the object logic. In this talk I will describe our work in the Iris project to address this problem - first for interactive proofs, and then for semi-automated proofs. The Iris Proof Mode provides high-level tactics for interactive proofs in higher-order concurrent separation logic with modalities. Recent work on RefinedC and Diaframe have built on top of the Iris Proof Mode to obtain proof automation for low-level C programs and fine-grained concurrent programs.
Cite as

Robbert Krebbers. Interactive and Automated Proofs in Modal Separation Logic (Invited Talk). In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{krebbers:LIPIcs.ITP.2023.2,
  author =	{Krebbers, Robbert},
  title =	{{Interactive and Automated Proofs in Modal Separation Logic}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{2:1--2:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.2},
  URN =		{urn:nbn:de:0030-drops-183770},
  doi =		{10.4230/LIPIcs.ITP.2023.2},
  annote =	{Keywords: Program Verification, Separation Logic, Step-Indexing, Modal Logic, Interactive Theorem Proving, Proof Automation, Iris, Coq}
}
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 Imprint Privacy Contact