Footprints in local reasoning

Mohammad Raza; Philippa Gardner

doi:10.1007/978-3-540-78499-9_15

Footprints in local reasoning

Mohammad Raza, Philippa Gardner

Imperial College London

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

4 Citations (Scopus)

Abstract

Local reasoning about programs exploits the natural local behaviour common in programs by focussing on the footprint - that part of the resource accessed by the program. We address the problem of formally characterising and analysing the footprint notion for abstract local functions introduced by Calcagno, O’Hearn and Yang. With our definition, we prove that the footprints are the only essential elements required for a complete specification of a local function. We also show that, for well-founded models (which is usually the case in practice), a smallest specification always exists that only includes the footprints, thus formalising the notion of small axioms in local reasoning. We also present results for the non-well-founded case, and introduce the natural class of one-step local functions for which the footprints are the smallest safe states.

Original language	English
Title of host publication	11th International Conference, FOSSACS 2008
Pages	201-215
Number of pages	15
DOIs	https://doi.org/10.1007/978-3-540-78499-9_15
Publication status	Published - 2009
Externally published	Yes
Event	"11th International Conferenceon the Foundations of Software Science and Computations Structures, FOSSACS 2008" - Budapest, Hungary Duration: 29 Mar 2008 → 6 Apr 2008

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	4962 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	"11th International Conferenceon the Foundations of Software Science and Computations Structures, FOSSACS 2008"
Country/Territory	Hungary
City	Budapest
Period	29/03/08 → 6/04/08

Keywords

footprints
separation logic
local reasoning

Access to Document

10.1007/978-3-540-78499-9_15

https://scholar.google.com/citations?view_op=view_citation&hl=en&user=VPEWcZcAAAAJ&pagesize=100&citation_for_view=VPEWcZcAAAAJ:9yKSN-GCB0IC

Cite this

@inproceedings{6d0064089ae9401ab332cd622ce4a722,

title = "Footprints in local reasoning",

abstract = "Local reasoning about programs exploits the natural local behaviour common in programs by focussing on the footprint - that part of the resource accessed by the program. We address the problem of formally characterising and analysing the footprint notion for abstract local functions introduced by Calcagno, O{\textquoteright}Hearn and Yang. With our definition, we prove that the footprints are the only essential elements required for a complete specification of a local function. We also show that, for well-founded models (which is usually the case in practice), a smallest specification always exists that only includes the footprints, thus formalising the notion of small axioms in local reasoning. We also present results for the non-well-founded case, and introduce the natural class of one-step local functions for which the footprints are the smallest safe states.",

keywords = "footprints, separation logic, local reasoning",

author = "Mohammad Raza and Philippa Gardner",

year = "2009",

doi = "10.1007/978-3-540-78499-9_15",

language = "English",

isbn = "3540784977",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "201--215",

booktitle = "11th International Conference, FOSSACS 2008",

note = "{"}11th International Conferenceon the Foundations of Software Science and Computations Structures, FOSSACS 2008{"} ; Conference date: 29-03-2008 Through 06-04-2008",

}

Raza, M & Gardner, P 2009, Footprints in local reasoning. in 11th International Conference, FOSSACS 2008. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4962 LNCS, pp. 201-215, "11th International Conferenceon the Foundations of Software Science and Computations Structures, FOSSACS 2008", Budapest, Hungary, 29/03/08. https://doi.org/10.1007/978-3-540-78499-9_15

Footprints in local reasoning. / Raza, Mohammad; Gardner, Philippa.
11th International Conference, FOSSACS 2008. 2009. p. 201-215 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4962 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Footprints in local reasoning

AU - Raza, Mohammad

AU - Gardner, Philippa

PY - 2009

Y1 - 2009

N2 - Local reasoning about programs exploits the natural local behaviour common in programs by focussing on the footprint - that part of the resource accessed by the program. We address the problem of formally characterising and analysing the footprint notion for abstract local functions introduced by Calcagno, O’Hearn and Yang. With our definition, we prove that the footprints are the only essential elements required for a complete specification of a local function. We also show that, for well-founded models (which is usually the case in practice), a smallest specification always exists that only includes the footprints, thus formalising the notion of small axioms in local reasoning. We also present results for the non-well-founded case, and introduce the natural class of one-step local functions for which the footprints are the smallest safe states.

AB - Local reasoning about programs exploits the natural local behaviour common in programs by focussing on the footprint - that part of the resource accessed by the program. We address the problem of formally characterising and analysing the footprint notion for abstract local functions introduced by Calcagno, O’Hearn and Yang. With our definition, we prove that the footprints are the only essential elements required for a complete specification of a local function. We also show that, for well-founded models (which is usually the case in practice), a smallest specification always exists that only includes the footprints, thus formalising the notion of small axioms in local reasoning. We also present results for the non-well-founded case, and introduce the natural class of one-step local functions for which the footprints are the smallest safe states.

KW - footprints

KW - separation logic

KW - local reasoning

UR - http://www.scopus.com/inward/record.url?scp=46449092589&partnerID=8YFLogxK

U2 - 10.1007/978-3-540-78499-9_15

DO - 10.1007/978-3-540-78499-9_15

M3 - Conference contribution

SN - 3540784977

SN - 9783540784975

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 201

EP - 215

BT - 11th International Conference, FOSSACS 2008

T2 - "11th International Conferenceon the Foundations of Software Science and Computations Structures, FOSSACS 2008"

Y2 - 29 March 2008 through 6 April 2008

ER -

Footprints in local reasoning

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this