Skip to main content

Connecting Higher-Order Separation Logic to a First-Order Outside World

Author(s): Mansky, William; Honoré, Wolf; Appel, Andrew W

Download
To refer to this page use: http://arks.princeton.edu/ark:/88435/pr16g03
Full metadata record
DC FieldValueLanguage
dc.contributor.authorMansky, William-
dc.contributor.authorHonoré, Wolf-
dc.contributor.authorAppel, Andrew W-
dc.date.accessioned2021-10-08T19:45:02Z-
dc.date.available2021-10-08T19:45:02Z-
dc.date.issued2020en_US
dc.identifier.citationMansky, William, Wolf Honoré, and Andrew W. Appel. "Connecting Higher-Order Separation Logic to a First-Order Outside World." In European Symposium on Programming (2020): pp. 428-455. doi:10.1007/978-3-030-44914-8_16en_US
dc.identifier.issn0302-9743-
dc.identifier.urihttp://arks.princeton.edu/ark:/88435/pr16g03-
dc.description.abstractSeparation logic is a useful tool for proving the correctness of programs that manipulate memory, especially when the model of memory includes higher-order state: Step-indexing, predicates in the heap, and higher-order ghost state have been used to reason about function pointers, data structure invariants, and complex concurrency patterns. On the other hand, the behavior of system features (e.g., operating systems) and the external world (e.g., communication between components) is usually specified using first-order formalisms. In principle, the soundness theorem of a separation logic is its interface with first-order theorems, but the soundness theorem may implicitly make assumptions about how other components are specified, limiting its use. In this paper, we show how to extend the higher-order separation logic of the Verified Software Toolchain to interface with a first-order verified operating system, in this case CertiKOS, that mediates its interaction with the outside world. The resulting system allows us to prove the correctness of C programs in separation logic based on the semantics of system calls implemented in CertiKOS. It also demonstrates that the combination of interaction trees + CompCert memories serves well as a lingua franca to interface and compose two quite different styles of program verification.en_US
dc.format.extent428 - 455en_US
dc.language.isoen_USen_US
dc.relation.ispartofEuropean Symposium on Programmingen_US
dc.relation.ispartofseriesLecture Notes in Computer Science;-
dc.rightsFinal published version. This is an open access article.en_US
dc.titleConnecting Higher-Order Separation Logic to a First-Order Outside Worlden_US
dc.typeConference Articleen_US
dc.identifier.doi10.1007/978-3-030-44914-8_16-
pu.type.symplectichttp://www.symplectic.co.uk/publications/atom-terms/1.0/conference-proceedingen_US

Files in This Item:
File Description SizeFormat 
ConnectingSepLogicFirstOrderOutsideWorld.pdf472.29 kBAdobe PDFView/Download


Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.