Position paper: the science of deep specification
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 compon...
| Main Authors: | , , , , , , |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | English |
| Published: |
The Royal Society
2019
|
| Online Access: | https://hdl.handle.net/1721.1/122621 |
| _version_ | 1826205819890302976 |
|---|---|
| author | Appel, Andrew W. Beringer, Lennart Chlipala, Adam Pierce, Benjamin C. Shao, Zhong Weirich, Stephanie Zdancewic, Steve |
| author2 | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory |
| author_facet | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Appel, Andrew W. Beringer, Lennart Chlipala, Adam Pierce, Benjamin C. Shao, Zhong Weirich, Stephanie Zdancewic, Steve |
| author_sort | Appel, Andrew W. |
| collection | MIT |
| description | 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’. |
| first_indexed | 2024-09-23T13:19:57Z |
| format | Article |
| id | mit-1721.1/122621 |
| institution | Massachusetts Institute of Technology |
| language | English |
| last_indexed | 2024-09-23T13:19:57Z |
| publishDate | 2019 |
| publisher | The Royal Society |
| record_format | dspace |
| spelling | mit-1721.1/1226212022-10-01T14:34:39Z Position paper: the science of deep specification Appel, Andrew W. Beringer, Lennart Chlipala, Adam Pierce, Benjamin C. Shao, Zhong Weirich, Stephanie Zdancewic, Steve Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science 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’. 2019-10-18T13:06:14Z 2019-10-18T13:06:14Z 2017-09 2019-10-04T16:10:46Z Article http://purl.org/eprint/type/JournalArticle 1364-503X 1471-2962 https://hdl.handle.net/1721.1/122621 Appel, Andrew W. et al. "Position paper: the science of deep specification." Philosophical Transactions of the Royal Society A 375, 2104: 20160331 © 2017 The Author(s) en http://dx.doi.org/10.1098/rsta.2016.0331 Philosophical Transactions of the Royal Society A Creative Commons Attribution-Noncommercial-Share Alike http://creativecommons.org/licenses/by-nc-sa/4.0/ application/pdf The Royal Society Prof. Chlipala via Phoebe Ayers |
| spellingShingle | Appel, Andrew W. Beringer, Lennart Chlipala, Adam Pierce, Benjamin C. Shao, Zhong Weirich, Stephanie Zdancewic, Steve Position paper: the science of deep specification |
| title | Position paper: the science of deep specification |
| title_full | Position paper: the science of deep specification |
| title_fullStr | Position paper: the science of deep specification |
| title_full_unstemmed | Position paper: the science of deep specification |
| title_short | Position paper: the science of deep specification |
| title_sort | position paper the science of deep specification |
| url | https://hdl.handle.net/1721.1/122621 |
| work_keys_str_mv | AT appelandreww positionpaperthescienceofdeepspecification AT beringerlennart positionpaperthescienceofdeepspecification AT chlipalaadam positionpaperthescienceofdeepspecification AT piercebenjaminc positionpaperthescienceofdeepspecification AT shaozhong positionpaperthescienceofdeepspecification AT weirichstephanie positionpaperthescienceofdeepspecification AT zdancewicsteve positionpaperthescienceofdeepspecification |