Write a Blog >>
Sun 20 - Fri 25 October 2019 Athens, Greece
Thu 24 Oct 2019 14:45 - 15:07 at Olympia - Specification and Certification Chair(s): Colin Gordon

In addition to pre- and postconditions, program specifications in recent separation logics for concurrency have employed an algebraic structure of \emph{resources}—a form of state transition systems—to describe the state-based program invariants that must be preserved, and to record the permissible atomic changes to program state. In this paper we introduce a novel notion of \emph{resource morphism}, i.e.~structure-preserving function on resources, and show how to effectively integrate it into separation logic, using an associated notion of morphism-specific \emph{simulation}. We apply morphisms and simulations to programs verified under one resource, to compositionally adapt them to operate under another resource, thus facilitating proof reuse.

Thu 24 Oct (GMT+03:00) Beirut change

14:00 - 15:30: OOPSLA - Specification and Certification at Olympia
Chair(s): Colin GordonDrexel University
splash-2019-oopsla14:00 - 14:22
Jia ChenUniversity of Texas at Austin, Jiayi WeiUniversity of Texas at Austin, Yu FengUniversity of California, Santa Barbara, Osbert BastaniUniversity of Pennsylvania, Isil DilligUniversity of Texas Austin
splash-2019-oopsla14:22 - 14:45
Timos AntonopoulosYale University, Eric KoskinenStevens Institute of Technology, Ton Chanh LeStevens Institute of Technology
splash-2019-oopsla14:45 - 15:07
Aleksandar NanevskiIMDEA Software Institute, Anindya BanerjeeIMDEA Software Institute, Germán Andrés DelbiancoIRIF - Université de Paris, Ignacio FábregasIMDEA Software Institute
Link to publication DOI
splash-2019-oopsla15:07 - 15:30
Shengyi WangNational University of Singapore, Qinxiang CaoShanghai Jiao Tong University, Anshuman MohanNational University of Singapore, Aquinas HoborNational University of Singapore
DOI Pre-print