Semantic analysis of pointer aliasing, allocation and disposal in Hoare logic

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Semantic analysis of pointer aliasing, allocation and disposal in Hoare logic

Full text

Pdf (350 KB)

Source

International Conference on Principles and Practice of Declarative Programming archive
Proceedings of the 2nd ACM SIGPLAN international conference on Principles and practice of declarative programming table of contents

Montreal, Quebec, Canada

Pages: 190 - 201

Year of Publication: 2000

ISBN:1-58113-265-4

Authors

Cristiano Calcagno	Department of Computer Science, QMW College and DISI, University of Genova
Samin Ishtiaq	Department of Computer Science, Queen Mary & Westfield College
Peter W. O'Hearn	Department of Computer Science, Queen Mary & Westfield College

Sponsor

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 3, Downloads (12 Months): 13, Citation Count: 5

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions 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/351268.351291 What is a DOI?

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	America, P. and de Boer, F. Reasoning about dyamically evolving process structures. Formal Aspects of Computing 6 (1994), 269{316.
	2	Barringer, H., Cheng, J. H., and Jones, C. B. A logic covering unde~nedness in program proofs. Acta Informatica 21 (1984), 251{269.
	3	Richard Bornat, Proving Pointer Programs in Hoare Logic, Proceedings of the 5th International Conference on Mathematics of Program Construction, p.102-126, July 03-05, 2000
	4	Burstall, R. Some techniques for proving correctness of programs which alter data structures. Machine Intelligence 7 (1972), 23{50.
	5	Cook, S. A. Soundness and completeness of an axiomatic system for program veri~cation. SIAM J. on Computing 7 (1978), 70{90.
	6	Frank S. de Boer, A WP-calculus for OO, Proceedings of the Second International Conference on Foundations of Software Science and Computation Structure, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'99, p.135-149, March 22-28, 1999
	7	C. A. R. Hoare , He Jifeng, A Trace Model for Pointers and Objects, Proceedings of the 13th European Conference on Object-Oriented Programming, p.1-17, June 14-18, 1999
	8	Hoare, C. A. R. and Wirth, N. An axiomatic de~nition of the programming language pascal. Acta Informatica 2 (1973), 335{355.
	9	Furio Honsell , Ian A. Mason , Scott Smith , Carolyn Talcott, A variable typed logic of effects, Information and Computation, v.119 n.1, p.55-90, May 15, 1995 [doi>10.1006/inco.1995.1077]
	10	Ishtiaq, S. and O'Hearn, P. BI as an assertion language for mutable data structures. Manuscript, March 2000.
	11	C. B. Jones, Partial functions and logics: a warning, Information Processing Letters, v.54 n.2, p.65-67, April 28, 1995 [doi>10.1016/0020-0190(95)00042-B]
	12	K. Rustan Leino, Toward reliable modular programs, California Institute of Technology, Pasadena, CA, 1995
	13	London, R. E. A. Proof rules for the programming language Euclid. Acta Informatica 10(1995), 1{26.
	14	Bernhard Möller, Calculating with pointer structures, Proceedings of the IFIP TC 2 WG 2.1 international workshop on Algorithmic languages and calculi, p.24-48, January 1997, Alsace, France
	15	Morris, J. A general axiom of assignment; Assignment and linked data structure; A proof of the Schorr-Waite algorithm. In Theoretical Foundations of Programming Methodology (1982), M. Broy andG.Schmidt, Eds., Reidel, pp. 25{51.
	16	Greg Nelson, Verifying reachability invariants of linked structures, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.38-47, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567073]
	17	Derek C. Oppen , Stephen A. Cook, Proving assertions about programs that manipulate data structures, Proceedings of seventh annual ACM symposium on Theory of computing, p.107-116, May 05-07, 1975, Albuquerque, New Mexico, United States [doi>10.1145/800116.803758]
	18	Reynolds, J. Intuitionistic reasoning about shared mutable data structure. To appear intheProceedings of the Symposium in Celebration of the Work of C.A.R. Hoare, 2000.
	19	R. D. Tennent, A note on undefined expression values in programming logics, Information Processing Letters, v.24 n.5, p.331-333, 16 March 1987 [doi>10.1016/0020-0190(87)90158-X]

CITED BY 5

	Samin S. Ishtiaq , Peter W. O'Hearn, BI as an assertion language for mutable data structures, ACM SIGPLAN Notices, v.36 n.3, p.14-26, March 2001
	Cristiano Calcagno , Peter O'Hearn , Richard Bornat, Program logic and equivalence in the presence of garbage collection, Theoretical Computer Science, v.298 n.3, p.557-581, 11 April 2003
	Noah Torp-Smith , Lars Birkedal , John C. Reynolds, Local reasoning about a copying garbage collector, ACM Transactions on Programming Languages and Systems (TOPLAS), v.30 n.4, p.1-58, July 2008
	Cristiano Calcagno, Stratified operational semantics for safety and correctness of the region calculus, ACM SIGPLAN Notices, v.36 n.3, p.155-165, March 2001
	A. V. Zamulin, Algebraic Semantics of an Imperative Programming Language, Programming and Computing Software, v.29 n.6, p.328-337, November-December 2003