3 Search Results for "Black, Sue"

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
DOI: 10.4230/DagSemProc.05451.11
Using Program Slicing to Identify Faults in Software

Authors: Sue Black, Steve Counsell, Tracy Hall, and Paul Wernick

Published in: Dagstuhl Seminar Proceedings, Volume 5451, Beyond Program Slicing (2006)

Abstract
This study explores the relationship between program slices and faults. The aim is to investigate whether the characteristics of program slices can be used to identify fault-prone software components. Slicing metrics and dependence clusters are used to characterise the slicing profile of a software component, then the relationship between the slicing profile of the component and the faults in that component are then analysed. Faults can increase the likelihood of a system becoming unstable causing problems for the development and evolution of the system. Identifying faultprone components is difficult and reliable predictors of faultproneness not easily identifiable. Program slicing is an established software engineering technique for the detection and correction of specific faults. An investigation is carried out into whether the use of program slicing can be extended as a reliable tool to predict fault-prone software components. Preliminary results are promising suggesting that slicing may offer valuable insights into fault-proneness.
Cite as

Sue Black, Steve Counsell, Tracy Hall, and Paul Wernick. Using Program Slicing to Identify Faults in Software. In Beyond Program Slicing. Dagstuhl Seminar Proceedings, Volume 5451, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{black_et_al:DagSemProc.05451.11,
  author =	{Black, Sue and Counsell, Steve and Hall, Tracy and Wernick, Paul},
  title =	{{Using Program Slicing to Identify Faults in Software}},
  booktitle =	{Beyond Program Slicing},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5451},
  editor =	{David W. Binkley and Mark Harman and Jens Krinke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05451.11},
  URN =		{urn:nbn:de:0030-drops-5873},
  doi =		{10.4230/DagSemProc.05451.11},
  annote =	{Keywords: Program slicing, slicing metrics, fault proneness, software quality}
}
Document
DOI: 10.4230/DagSemProc.05451.4
And Now For Something Completely Different...

Authors: Sue Black and Philipp Bouillon

Published in: Dagstuhl Seminar Proceedings, Volume 5451, Beyond Program Slicing (2006)

Abstract
A pilot experiment was conducted at Dagstuhl using the 'Beyond program slicing' seminar attendees. Attendees were split into three groups: all were given the same program to understand and a list of program comprehension related questions to answer. Group one had only the source code, group two had the source code and the dynamic trace of the program, group three had the source and a control-flow graph of the program.
Cite as

Sue Black and Philipp Bouillon. And Now For Something Completely Different.... In Beyond Program Slicing. Dagstuhl Seminar Proceedings, Volume 5451, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{black_et_al:DagSemProc.05451.4,
  author =	{Black, Sue and Bouillon, Philipp},
  title =	{{And Now For Something Completely Different...}},
  booktitle =	{Beyond Program Slicing},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5451},
  editor =	{David W. Binkley and Mark Harman and Jens Krinke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05451.4},
  URN =		{urn:nbn:de:0030-drops-5833},
  doi =		{10.4230/DagSemProc.05451.4},
  annote =	{Keywords: Group experiment, program comprehension, source code, dynamic trace, control flow graph}
}
  • Refine by Author
  • 2 Black, Sue
  • 1 Bouillon, Philipp
  • 1 Counsell, Steve
  • 1 Hall, Tracy
  • 1 Hermes, Marc
  • Show More...

  • Refine by Classification
  • 1 Theory of computation → Data structures design and analysis
  • 1 Theory of computation → Hoare logic
  • 1 Theory of computation → Programming logic
  • 1 Theory of computation → Separation logic

  • Refine by Keyword
  • 1 Coq
  • 1 Data Structures
  • 1 Group experiment
  • 1 Iris
  • 1 Program Verification
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 2 2006
  • 1 2024

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