Article

Reasoning about iterators with separation logic

Author:

Neelakantan R. KrishnaswamiAuthors Info & Claims

SAVCBS '06: Proceedings of the 2006 conference on Specification and verification of component-based systems

Pages 83 - 86

https://doi.org/10.1145/1181195.1181213

Published: 10 November 2006 Publication History

Get Access

Abstract

Separation logic is an extension of Hoare logic which permits reasoning about imperative programs that use shared mutable heap structure. In this note, we show how to use higher-order separation logic to reason abstractly about an iterator protocol.

References

[1]

J. Berdine, C. Calcagno, and P. W. O'Hearn. Smallfoot: Modular automatic assertion checking with separation logic. In Proceedings of the Fourth International Symposium on Formal Methods for Components and Objects, Amsterdam, The Netherlands, 2001.

Digital Library

Google Scholar

[2]

B. Biering, L. Birkedal, and N. Torp-Smith. BI-hyperdoctrines and higher order separation logic. In Proc. of ESOP 2005: The European Symposium on Programming, pages 233--247, Edinburgh, Scotland, April 2005.

Digital Library

Google Scholar

[3]

E. Gamma, R. Helm, R. Johnson, and J. Vlissides. Design Patterns. Elements of reusable object-oriented software. Addison-Wesley, 1995.

Digital Library

Google Scholar

[4]

C. A. R. Hoare. An axiomatic approach to computer programming. Communications of the ACM, 12(583):576--580, 1969.

Digital Library

Google Scholar

[5]

S. Ishtiaq and P. W. O'Hearn. BI as an assertion language for mutable data structures. In Proceedings of the 28th Annual ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages (POPL'01), London, 2001.

Digital Library

Google Scholar

[6]

J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In Proc. of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS'02), pages 55--74, Copenhagen, Denmark, July 2002. IEEE Press.

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
Dardinier TParthasarathy GWeeks NMüller PSummers A(2022)Sound Automation of Magic WandsComputer Aided Verification10.1007/978-3-031-13188-2_7(130-151)Online publication date: 6-Aug-2022
https://doi.org/10.1007/978-3-031-13188-2_7
Show More Cited By

Index Terms

Reasoning about iterators with separation logic
1. Software and its engineering

Recommendations

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 ...
Interactive proofs in higher-order concurrent separation logic
POPL '17

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 ...
Two-Variable Separation Logic and Its Inner Circle

Separation logic is a well-known assertion language for Hoare-style proof systems. We show that first-order separation logic with a unique record field restricted to two quantified variables and no program variables is undecidable. This is among the ...

Comments

Information & Contributors

Information

Published In

SAVCBS '06: Proceedings of the 2006 conference on Specification and verification of component-based systems

November 2006

87 pages

ISBN:159593586X

DOI:10.1145/1181195

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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 10 November 2006

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

SIGSOFT06/FSE-14

Sponsor:

SIGSOFT

SIGSOFT06/FSE-14: SIGSOFT 2006 -14th International Symposium on the Foundations of Software Engineering

November 10 - 11, 2006

Oregon, Portland

Acceptance Rates

SAVCBS '06 Paper Acceptance Rate 14 of 14 submissions, 100%;

Overall Acceptance Rate 37 of 46 submissions, 80%

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

29
Total Citations
View Citations
227
Total Downloads

Downloads (Last 12 months)5
Downloads (Last 6 weeks)1

Reflects downloads up to 25 Dec 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
Dardinier TParthasarathy GWeeks NMüller PSummers A(2022)Sound Automation of Magic WandsComputer Aided Verification10.1007/978-3-031-13188-2_7(130-151)Online publication date: 6-Aug-2022
https://doi.org/10.1007/978-3-031-13188-2_7
Hóu ZClouston RGoré RTiu A(2018)Modular Labelled Sequent Calculi for Abstract Separation LogicsACM Transactions on Computational Logic10.1145/319738319:2(1-35)Online publication date: 28-Apr-2018
https://dl.acm.org/doi/10.1145/3197383
Hóu ZTiu A(2016)Completeness for a First-Order Abstract Separation LogicProgramming Languages and Systems10.1007/978-3-319-47958-3_23(444-463)Online publication date: 9-Oct-2016
https://doi.org/10.1007/978-3-319-47958-3_23
Hóu ZGoré RTiu A(2015)Automated Theorem Proving for Assertions in Separation Logic with All ConnectivesAutomated Deduction - CADE-2510.1007/978-3-319-21401-6_34(501-516)Online publication date: 25-Jul-2015
https://doi.org/10.1007/978-3-319-21401-6_34
Lee WPark S(2014)A proof system for separation logic with magic wandACM SIGPLAN Notices10.1145/2578855.253587149:1(477-490)Online publication date: 8-Jan-2014
https://dl.acm.org/doi/10.1145/2578855.2535871
Hóu ZClouston RGoré RTiu A(2014)Proof search for propositional abstract separation logics via labelled sequentsACM SIGPLAN Notices10.1145/2578855.253586449:1(465-476)Online publication date: 8-Jan-2014
https://dl.acm.org/doi/10.1145/2578855.2535864
Lee WPark SJagannathan SSewell P(2014)A proof system for separation logic with magic wandProceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages10.1145/2535838.2535871(477-490)Online publication date: 11-Jan-2014
https://dl.acm.org/doi/10.1145/2535838.2535871
Hóu ZClouston RGoré RTiu AJagannathan SSewell P(2014)Proof search for propositional abstract separation logics via labelled sequentsProceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages10.1145/2535838.2535864(465-476)Online publication date: 11-Jan-2014
https://dl.acm.org/doi/10.1145/2535838.2535864
Show More Cited By

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

Interactive proofs in higher-order concurrent separation logic

Interactive proofs in higher-order concurrent separation logic

Two-Variable Separation Logic and Its Inner Circle

Comments

Published In

Sponsors

Publisher

Publication History

Permissions

Check for updates

Author Tags

Qualifiers

Conference

Acceptance Rates

Other Metrics

Article Metrics

Other Metrics

Cited By

Login options

Full Access

PDF

eReader

Abstract

References

Cited By

Index Terms

Recommendations

Interactive proofs in higher-order concurrent separation logic

Interactive proofs in higher-order concurrent separation logic

Two-Variable Separation Logic and Its Inner Circle

Comments

Information

Published In

Sponsors

Publisher

Publication History

Permissions

Check for updates

Author Tags

Qualifiers

Conference

Acceptance Rates

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

Login options

Full Access

View options

PDF

eReader

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations