More Web Proxy on the site http://driver.im/

Article

Storeless semantics and alias logic

Authors:

Yassine LaknechAuthors Info & Claims

PEPM '03: Proceedings of the 2003 ACM SIGPLAN workshop on Partial evaluation and semantics-based program manipulation

Pages 55 - 65

https://doi.org/10.1145/777388.777395

Published: 07 June 2003 Publication History

Abstract

Pioneering work has been done by Jonkers [18] to define a semantics of pointer manipulating programs that is abstract in the sense of ignoring low-level aspects such as dangling pointers and garbage objects. We explore the principles of such storeless semantics from a logical point of view, first defining a simple logic to completely characterize heap structures up to isomorphism. Second, we extend this language to a full-blown alias logic (AL) that allows to express regular properties of unbounded heap structures. Along the development, we present an operational storeless semantics and give sound and complete total correctness axioms for deterministic programs in the form of Hoare triples, using AL.

References

[1]

M. Benedikt, T. Reps and M. Sagiv: A Decidable Logic for Describing Linked Data Structures. In Proc. European Symposium On Programming (1999).]]

Digital Library

[2]

Marius Bozga, Radu Iosif and Yassine Lakhnech: Storeless Semantics and Alias Logic. Technical report, http://www-verimag.imag.fr/˜bozga/ssal.ps]]

[3]

C. Calcagno and P.W. O'Hearn: On Garbage and Program Logic. Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science, Volume 2030 (2001) pp 137--151]]

Digital Library

[4]

C. Calcagno, H. Yang and P.W. O'Hearn: Computability and Complexity Results for a Spatial Assertion Language for Data Structures. In FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science, Lecture Notes in Computer Science, Volume 2245 (2001), pp 108--119]]

Digital Library

[5]

Frank S. de Boer. Reasoning about dynamically evolving process structures. Ph.D. Thesis, Vrije Universiteit te Amsterdam (University of Amsterdam), 1991.]]

[6]

Edmund M. Clarke, Somesh Jha, Reinhard Enders and Thomas Filkorn: Exploiting Symmetry In Temporal Logic Model Checking. Formal Methods in System Design, Vol.9, No. 1/2 (1996) 77--104]]

Digital Library

[7]

Alain Deutsch. A storeless model of aliasing and its abstractions using finite representations of right-regular equivalence relations. In Proceedings of the IEEE 1992 Conference on Computer Languages (April 1992) pp. 2--13]]

[8]

Alain Deutsch. Interprocedural May-Alias Analysis for Pointers: Beyond k-limiting. In Proceedings of the ACM SIGPLAN'94 Conference on Programming Language Design and Implementation (PLDI), Orlando, Florida, June 20-24, 1994. SIGPLAN Notices 29(6) (June 1994) pp. 230--241]]

Digital Library

[9]

Edsger W. Dijkstra and Carel S. Scholten. Predicate Calculus and Program Semantics. Springer-Verlag, New York 1990.]]

Digital Library

[10]

Samuel Eilenberg. Automata, Languages, and Machines. Academic Press (1976)]]

Digital Library

[11]

E. Emerson and A. P. Sistla: Symmetry and Model Checking. Formal Methods in System Design, Vol.9, No. 1/2 (1996) 105--131]]

Digital Library

[12]

Radu Iosif: Symmetry Reductions for Model Checking of Concurrent Dynamic Software. Submitted, http://www-verimag.imag.friosif/papers.html]]

[13]

R. Ghiya and L. Hendren: Is it a Tree, a DAG or a Cyclic Graph? A Shape Analysis for Heap-Directed Pointers in C. In Proc. 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, (1996).]]

Digital Library

[14]

L. Hendren, J. Hummel and A. Nicolau: Abstractions for Recursive Pointer Data Structures: Improving the Analysis and Transformation of Imperative Programs. In Proc. ACM SIGPLAN Conference on Programming Languages Design and Implementation, (1992).]]

Digital Library

[15]

M. Hennessy and R. Milner: Algebraic Laws for Nondeterminism and Concurrency. Journal of the ACM Vol. 32 (1985) pp. 137--161]]

Digital Library

[16]

C.A.R Hoare and He Jifeng: A Trace Model for Pointers and Objects. In Proc. ECOOP'99, Lecture Notes in Computer Science, Vol. 1628, pp. 1--18 (1999)]]

Digital Library

[17]

Samin Ishtiaq and Peter O'Hearn: BI as an Assertion Language for Mutable Data Structures. Proc. of 28th ACM-SIGPLAN Symposium on Principles of Programming Languages (2001)]]

Digital Library

[18]

H. B. M. Jonkers. Abstract Storage Structures. Algorithmic Languages, North-Holland (1981)]]

[19]

N. Klarlund and M. I. Schwartzbach: In Proc. 20th Annual Symposium on Principles of Programming Languages (1993) pp. 196--205]]

Digital Library

[20]

N. Klarlund and M. I. Schwartzbach: Graphs and Decidable Transductions Based on Edge Constraints, In Proc. 19th Colloquium on Trees and Algebra in Programming, Lecture Notes in Computer Science, Volume 787 (1994) pp. 187--201]]

Digital Library

[21]

John C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. Proc 17th IEEE Symposium on Logic in Computer Science (2002)]]

Digital Library

[22]

P.W. O'Hearn and D.J. Pym: The Logic of Bunched Implications. Bulletin of Symbolic Logic, 5(2) (1999) pp. 215--244]]

[23]

P.W. O'Hearn, J.C. Reynolds and H. Yang: Local reasoning about programs that alter data structures. Computer Science Logic, Lecture Notes in Computer Science, Volume 2142 (2001) pp 1--19]]

Digital Library

[24]

A. Moeller and M. I. Schwartzbach: The Pointer Assertion Logic Engine. In Proc. ACM SIGPLAN Conference on Programming Languages Design and Implementation, (2001).]]

Digital Library

[25]

M. Sagiv, M., T. Reps and R. Wilhelm. Parametric Shape Analysis via 3-Valued Logic. Conference Record of the Twenty-Third ACM Symposium on Principles of Programming Languages, (San Antonio, TX, Jan. 20-22, 1999), ACM, New York, NY, 1999.]]

Digital Library

Cited By

Rinetzky NBauer JReps TSagiv MWilhelm R(2019)A semantics for procedure local heaps and its abstractionsACM SIGPLAN Notices10.1145/1047659.104033040:1(296-309)Online publication date: 27-Feb-2019
https://dl.acm.org/doi/10.1145/1047659.1040330
Qin SHe GChin WCraciun FHe MMing Z(2017)Automated specification inference in a combined domain via user-defined predicatesScience of Computer Programming10.1016/j.scico.2017.05.007148:C(189-212)Online publication date: 15-Nov-2017
https://dl.acm.org/doi/10.1016/j.scico.2017.05.007
Nicolay JStiévenart QDe Meuter WDe Roover C(2017)Purity analysis for JavaScript through abstract interpretationJournal of Software: Evolution and Process10.1002/smr.188929:12(e1889)Online publication date: 25-Aug-2017
https://doi.org/10.1002/smr.1889
Show More Cited By

Index Terms

Storeless semantics and alias logic
1. Theory of computation
  1. Logic
  2. Semantics and reasoning
    1. Program reasoning

Recommendations

Storeless semantics and alias logic
Proceedings of the ACM SIGPLAN symposium on principles and practice of parallel programming (PPoPP 2003) and workshop on partial evaluation and semantics-based program manipulation (PEPM 2003)

Pioneering work has been done by Jonkers [18] to define a semantics of pointer manipulating programs that is abstract in the sense of ignoring low-level aspects such as dangling pointers and garbage objects. We explore the principles of such storeless ...
Semantics for disjunctive logic programs
A Mechanical Analysis of Program Verification Strategies

We analyze three proof strategies commonly used in deductive verification of deterministic sequential programs formalized with operational semantics. The strategies are (i) stepwise invariants , (ii) clock functions , and (iii) inductive assertions . ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PEPM '03: Proceedings of the 2003 ACM SIGPLAN workshop on Partial evaluation and semantics-based program manipulation

June 2003

100 pages

ISBN:1581136676

DOI:10.1145/777388

Program Chair:
Michael Leuschel
University of Southampton, UK

ACM SIGPLAN Notices Volume 38, Issue 10
Proceedings of the ACM SIGPLAN symposium on principles and practice of parallel programming (PPoPP 2003) and workshop on partial evaluation and semantics-based program manipulation (PEPM 2003)
October 2003
331 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/966049
Issue’s Table of Contents

Copyright © 2003 ACM.

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]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 07 June 2003

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

PEPM03

Sponsor:

PEPM03: Partial Evaluation and Semantics-Based Program Manipulation

June 7, 2003

California, San Diego, USA

Acceptance Rates

Overall Acceptance Rate 66 of 120 submissions, 55%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

22
Total Citations
View Citations
369
Total Downloads

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

Reflects downloads up to 01 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Rinetzky NBauer JReps TSagiv MWilhelm R(2019)A semantics for procedure local heaps and its abstractionsACM SIGPLAN Notices10.1145/1047659.104033040:1(296-309)Online publication date: 27-Feb-2019
https://dl.acm.org/doi/10.1145/1047659.1040330
Qin SHe GChin WCraciun FHe MMing Z(2017)Automated specification inference in a combined domain via user-defined predicatesScience of Computer Programming10.1016/j.scico.2017.05.007148:C(189-212)Online publication date: 15-Nov-2017
https://dl.acm.org/doi/10.1016/j.scico.2017.05.007
Nicolay JStiévenart QDe Meuter WDe Roover C(2017)Purity analysis for JavaScript through abstract interpretationJournal of Software: Evolution and Process10.1002/smr.188929:12(e1889)Online publication date: 25-Aug-2017
https://doi.org/10.1002/smr.1889
Qin SHe GChin WYang H(2013)Invariants synthesis over a combined domain for automated program verificationTheories of Programming and Formal Methods10.5555/2554641.2554660(304-325)Online publication date: 1-Jan-2013
https://dl.acm.org/doi/10.5555/2554641.2554660
He GQin SChin WCraciun F(2013)Automated Specification Discovery via User-Defined PredicatesFormal Methods and Software Engineering10.1007/978-3-642-41202-8_26(397-414)Online publication date: 2013
https://doi.org/10.1007/978-3-642-41202-8_26
Qin SHe GChin WYang H(2013)Invariants Synthesis over a Combined Domain for Automated Program VerificationTheories of Programming and Formal Methods10.1007/978-3-642-39698-4_19(304-325)Online publication date: 2013
https://doi.org/10.1007/978-3-642-39698-4_19
Wang ZChen YWang ZWang WTian B(2008)An Extension to Pointer Logic for VerificationProceedings of the 2008 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering10.1109/TASE.2008.13(49-56)Online publication date: 17-Jun-2008
https://dl.acm.org/doi/10.1109/TASE.2008.13
Wang ZChen YWang ZWang WTian B(2008)Implementation of Pointer Logic for Automated VerificationProceedings of the 2008 The 9th International Conference for Young Computer Scientists10.1109/ICYCS.2008.168(2295-2301)Online publication date: 18-Nov-2008
https://dl.acm.org/doi/10.1109/ICYCS.2008.168
Wang ZChen YWang ZHua B(2008)Automated verification of pointer programs in pointer logicFrontiers of Computer Science in China10.1007/s11704-008-0033-82:4(380-397)Online publication date: 5-Nov-2008
https://doi.org/10.1007/s11704-008-0033-8
Češka MErlebach PVojnar T(2007)Generalised multi-pattern-based verification of programs with linear linked structuresFormal Aspects of Computing10.1007/s00165-007-0031-x19:3(363-374)Online publication date: 30-Mar-2007
https://doi.org/10.1007/s00165-007-0031-x
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.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents