Reasoning about iterators with separation logic

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Reasoning about iterators with separation logic

Full text

Pdf (212 KB)

Source

International Conference on Software Engineering archive
Proceedings of the 2006 conference on Specification and verification of component-based systems table of contents

Portland, Oregon

SESSION: Challenge problem solutions table of contents

Pages: 83 - 86

Year of Publication: 2006

ISBN:1-59593-586-X

Author

Neelakantan R. Krishnaswami

Carnegie Mellon University

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 5, Downloads (12 Months): 16, Citation Count: 2

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1181195.1181213 What is a DOI?

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

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked 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.
	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.
	3	Erich Gamma , Richard Helm , Ralph Johnson , John Vlissides, Design patterns: elements of reusable object-oriented software, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1995
	4	C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
	5	Samin S. Ishtiaq , Peter W. O'Hearn, BI as an assertion language for mutable data structures, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.14-26, January 2001, London, United Kingdom
	6	John C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.55-74, July 22-25, 2002

CITED BY 2

	Nicolas Blanc , Alex Groce , Daniel Kroening, Verifying C++ with STL containers via predicate abstraction, Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering, November 05-09, 2007, Atlanta, Georgia, USA
	Neelakantan R. Krishnaswami , Jonathan Aldrich , Lars Birkedal , Kasper Svendsen , Alexandre Buisse, Design patterns in separation logic, Proceedings of the 4th international workshop on Types in language design and implementation, January 24-24, 2009, Savannah, GA, USA