TY - JOUR
T1 - Position paper
T2 - the science of deep specification
AU - Appel, Andrew W.
AU - Beringer, Lennart
AU - Chlipala, Adam
AU - Pierce, Benjamin C.
AU - Shao, Zhong
AU - Weirich, Stephanie
AU - Zdancewic, Steve
N1 - Funding Information:
Data accessibility. This article has no additional data. Competing interests. We declare we have no competing interests. Funding. The Science of Deep Specification is a Collaborative Research: Expeditions in Computing project funded by the National Science Foundation (NSF) under the awards 1521602 (A.W.A), 1521584 (A.C.), 1521539 (S.W., S.Z., B.C.P.) and 1521523 (Z.S.). Acknowledgements. We thank the graduate students and post-doctoral researchers of our research groups for their contributions, and our external academic and industrial collaborators for their participation. The comments we received from the editor and the anonymous referees were particularly helpful in shaping our presentation.
Publisher Copyright:
© 2017 The Author(s) Published by the Royal Society. All rights reserved.
PY - 2017/10/13
Y1 - 2017/10/13
N2 - We 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. This article is part of the themed issue ‘Verified trustworthy software systems’.
AB - We 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. This article is part of the themed issue ‘Verified trustworthy software systems’.
KW - Formal methods
KW - Programming languages
KW - Proof assistants
UR - http://www.scopus.com/inward/record.url?scp=85028945294&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85028945294&partnerID=8YFLogxK
U2 - 10.1098/rsta.2016.0331
DO - 10.1098/rsta.2016.0331
M3 - Article
C2 - 28871056
AN - SCOPUS:85028945294
SN - 1364-503X
VL - 375
JO - Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences
JF - Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences
IS - 2104
M1 - 20160331
ER -