research-article

Modular verification of linked lists with views via separation logic

Authors:

Jonas Braband Jensen,

Lars Birkedal,

Peter SestoftAuthors Info & Claims

FTFJP '10: Proceedings of the 12th Workshop on Formal Techniques for Java-Like Programs

Article No.: 4, Pages 1 - 7

https://doi.org/10.1145/1924520.1924524

Published: 22 June 2010 Publication History

Get Access

Abstract

We present a separation logic specification and verification of linked lists with views, a data structure from the C5 collection library for C#. A view is a generalization of the well-known concept of an iterator. Linked lists with views form an interesting case study for verification since they allow mutation of multiple possibly-overlapping views of the same underlying list. For modularity, we present our specification in a fragment of higher-order separation logic and use abstract predicates to give a specification with respect to which clients can be proved correct. We introduce a novel mathematical model of lists with views, and formulate succinct modular abstract specifications of the operations on the data structure. To show that the concrete implementation realizes the specification, we use fractional permissions in a novel way to capture the sharing of data between views and their underlying list.

We conclude by suggesting directions for future research that arose from conducting this case study.

References

[1]

A. Banerjee, D. Naumann, and S. Rosenberg. Regional logic for local reasoning about global invariants. In Proceedings of ECOOP, 2008.

Digital Library

Google Scholar

[2]

B. Biering, L. Birkedal, and N. Torp-Smith. BI hyperdoctrines and higher-order separation logic. In Proceedings of ESOP, 2005.

Digital Library

Google Scholar

[3]

R. Bornat, C. Calcagno, P. O'Hearn, and M. Parkinson. Permission accounting in separation logic. In Proceedings of POPL, 2005.

Digital Library

Google Scholar

[4]

J. Boyland, W. Retert, and Y. Zhao. Iterators can be independent "from" their collections. In Proceedings of ECOOP, 2007.

Google Scholar

[5]

C. Calcagno, M. J. Parkinson, and V. Vafeiadis. Modular safety checking for fine-grained concurrency. In Proceedings of SAS, 2007.

Digital Library

Google Scholar

[6]

T. Dinsdale-Young, M. Dodds, P. Gardner, M. J. Parkinson, and V. Vafeiadis. Concurrent abstract predicates. In Proceedings of ECOOP, 2010.

Digital Library

Google Scholar

[7]

C. Haack and C. Hurlin. Resource usage protocols for iterators. In Proceedings of IWACO, 2008.

Google Scholar

[8]

J. B. Jensen. Specification and validation of data structures using separation logic. Master's thesis, Technical University of Denmark, February 2010.

Google Scholar

[9]

N. Kokholm and P. Sestoft. The C5 generic collection library for C# and CLI. Technical Report ITU-TR-2006-76, IT University of Copenhagen, 2006.

Google Scholar

[10]

N. R. Krishnaswami, J. Aldrich, L. Birkedal, K. Svendsen, and A. Buisse. Design patterns in separation logic. In Proceedings of TLDI, 2009.

Digital Library

Google Scholar

[11]

M. Parkinson. Local Reasoning for Java. PhD thesis, University of Cambridge, 2005.

Google Scholar

[12]

M. Parkinson and G. Bierman. Separation logic and abstraction. In Proceedings of POPL, 2005.

Digital Library

Google Scholar

[13]

J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In Proceedings of LICS, 2002.

Digital Library

Google Scholar

[14]

K. Svendsen, L. Birkedal, and M. Parkinson. Verifying generics and delegates. In Proceedings of ECOOP, 2010.

Digital Library

Google Scholar

Cited By

View all

Blázquez JMontenegro MSegura C(2023)Verification of mutable linear data structures and iterator-based algorithms in DafnyJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2023.100875134(100875)Online publication date: Aug-2023
https://doi.org/10.1016/j.jlamp.2023.100875
Dardinier TMüller PSummers A(2022)Fractional resources in unbounded separation logicProceedings of the ACM on Programming Languages10.1145/35633266:OOPSLA2(1066-1092)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563326
Bengtson JJensen JSieczkowski FBirkedal L(2011)Verifying object-oriented programs with higher-order separation logic in CoqProceedings of the Second international conference on Interactive theorem proving10.5555/2033939.2033946(22-38)Online publication date: 22-Aug-2011
https://dl.acm.org/doi/10.5555/2033939.2033946
Show More Cited By

Index Terms

Recommendations

Quantitative Separation Logic and Programs with Lists

This paper presents an extension of a decidable fragment of Separation Logic for singly-linked lists, defined by Berdine et al. (2004). Our main extension consists in introducing atomic formulae of the form ls ^k( x , y ) describing a list ...
Unifying separation logic and region logic to allow interoperability
Abstract
Framing is important for specification and verification, especially in programs that mutate data structures with shared data, such as DAGs. Both separation logic and region logic are successful approaches to framing, with separation logic ...
Interactive proofs in higher-order concurrent separation logic
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

When using a proof assistant to reason in an embedded logic -- like separation logic -- one cannot benefit from the proof contexts and basic tactics of the proof assistant. This results in proofs that are at a too low level of abstraction because they ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

FTFJP '10: Proceedings of the 12th Workshop on Formal Techniques for Java-Like Programs

June 2010

66 pages

ISBN:9781450305402

DOI:10.1145/1924520

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 22 June 2010

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ECOOP '10

Sponsor:

AITO

ECOOP '10: European Conference on Object-Oriented Programming

June 22, 2010

Maribor, Slovenia

Acceptance Rates

Overall Acceptance Rate 51 of 75 submissions, 68%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
146
Total Downloads

Downloads (Last 12 months)4
Downloads (Last 6 weeks)0

Reflects downloads up to 24 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Blázquez JMontenegro MSegura C(2023)Verification of mutable linear data structures and iterator-based algorithms in DafnyJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2023.100875134(100875)Online publication date: Aug-2023
https://doi.org/10.1016/j.jlamp.2023.100875
Dardinier TMüller PSummers A(2022)Fractional resources in unbounded separation logicProceedings of the ACM on Programming Languages10.1145/35633266:OOPSLA2(1066-1092)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563326
Bengtson JJensen JSieczkowski FBirkedal L(2011)Verifying object-oriented programs with higher-order separation logic in CoqProceedings of the Second international conference on Interactive theorem proving10.5555/2033939.2033946(22-38)Online publication date: 22-Aug-2011
https://dl.acm.org/doi/10.5555/2033939.2033946
Mehnert H(2011)KopitiamProceedings of the Third international conference on NASA Formal methods10.5555/1986308.1986354(518-524)Online publication date: 18-Apr-2011
https://dl.acm.org/doi/10.5555/1986308.1986354
Mehnert H(2011)Kopitiam: Modular Incremental Interactive Full Functional Static Verification of Java CodeNASA Formal Methods10.1007/978-3-642-20398-5_42(518-524)Online publication date: 2011
https://doi.org/10.1007/978-3-642-20398-5_42

View Options

Login options

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

Cited By

Index Terms

Recommendations

Quantitative Separation Logic and Programs with Lists

Unifying separation logic and region logic to allow interoperability

Interactive proofs in higher-order concurrent separation logic