An Abstract Separation Logic for Interlinked Extensible Records

Martin Bodin 1 Thomas Jensen 1 Alan Schmitt 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : The memory manipulated by JavaScript programs can be seen as a heap of extensible records storing values and pointers. We define a separation logic for describing such structures. In order to scale up to full-fledged languages such as JavaScript, this logic must be integrated with existing abstract domains from abstract interpretation. However, the frame rule—which is a central notion in separation logic—does not easily mix with abstract interpretation. We present a domain of heaps of interlinked extensible records based on both separation logic and abstract interpretation. The domain features spatial conjunction and uses summary nodes from shape analyses. We show how this domain can accommodate an abstract interpretation including a frame rule.
Document type :
Conference papers
Liste complète des métadonnées

https://hal.archives-ouvertes.fr/hal-01333600
Contributor : Julien Signoles <>
Submitted on : Thursday, September 15, 2016 - 11:07:29 AM
Last modification on : Wednesday, February 20, 2019 - 2:32:07 PM
Document(s) archivé(s) le : Friday, December 16, 2016 - 12:57:47 PM

File

main.pdf
Explicit agreement for this submission

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

  • HAL Id : hal-01333600, version 1

Citation

Martin Bodin, Thomas Jensen, Alan Schmitt. An Abstract Separation Logic for Interlinked Extensible Records. Vingt-septièmes Journées Francophones des Langages Applicatifs (JFLA 2016), Jan 2016, Saint-Malo, France. ⟨hal-01333600⟩

Share

Metrics

Record views

2499

Files downloads

67