Skip to main content

Position paper: the science of deep specification

Author(s): Appel, Andrew W; Beringer, Lennart; Chlipala, Adam; Pierce, Benjamin C; Shao, Zhong; et al

To refer to this page use:
Full metadata record
DC FieldValueLanguage
dc.contributor.authorAppel, Andrew W-
dc.contributor.authorBeringer, Lennart-
dc.contributor.authorChlipala, Adam-
dc.contributor.authorPierce, Benjamin C-
dc.contributor.authorShao, Zhong-
dc.contributor.authorWeirich, Stephanie-
dc.contributor.authorZdancewic, Steve-
dc.identifier.citationAppel, Andrew W., Lennart Beringer, Adam Chlipala, Benjamin C. Pierce, Zhong Shao, Stephanie Weirich, and Steve Zdancewic. "Position paper: the science of deep specification." Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences 375, no. 2104 (2017): 20160331. doi:10.1098/rsta.2016.0331en_US
dc.description.abstractWe introduce our efforts within the project ‘The science of deep specification’ to work out the key formal underpinnings of industrial-scale formal specifications of software and hardware components, anticipating a world where large verified systems are routinely built out of smaller verified components that are also used by many other projects. We identify an important class of specification that has already been used in a few experiments that connect strong component-correctness theorems across the work of different teams. To help popularize the unique advantages of that style, we dub it deep specification, and we say that it encompasses specifications that are rich, two-sided, formal and live (terms that we define in the article). Our core team is developing a proof-of-concept system (based on the Coq proof assistant) whose specification and verification work is divided across largely decoupled subteams at our four institutions, encompassing hardware microarchitecture, compilers, operating systems and applications, along with cross-cutting principles and tools for effective specification. We also aim to catalyse interest in the approach, not just by basic researchers but also by users in industry.en_US
dc.relation.ispartofPhilosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciencesen_US
dc.rightsAuthor's manuscripten_US
dc.titlePosition paper: the science of deep specificationen_US
dc.typeJournal Articleen_US

Files in This Item:
File Description SizeFormat 
PositionPaperDeepSpecification.pdf425.84 kBAdobe PDFView/Download

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