Position paper: the science of deep specification
Autor: | Zhong Shao, Steve Zdancewic, Stephanie Weirich, Adam Chlipala, Lennart Beringer, Benjamin C. Pierce, Andrew W. Appel |
---|---|
Přispěvatelé: | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory, Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science |
Jazyk: | angličtina |
Rok vydání: | 2017 |
Předmět: |
business.industry
General Mathematics General Engineering General Physics and Astronomy 0102 computer and information sciences 02 engineering and technology Articles Formal methods 01 natural sciences Software Work (electrical) 010201 computation theory & mathematics 020204 information systems Formal specification 0202 electrical engineering electronic engineering information engineering Key (cryptography) Position paper Software engineering business Mathematics |
Zdroj: | Prof. Chlipala via Phoebe Ayers BASE-Bielefeld Academic Search Engine |
Popis: | 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 itdeep specification, and we say that it encompasses specifications that arerich,two-sided,formalandlive(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’. |
Databáze: | OpenAIRE |
Externí odkaz: |
načítá se...