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
Times are displayed in time zone: (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