Authors
Lennart Beringer
Adam Chlipala
Benjamin Pierce
Zhong Shao
Stephanie Weirich
Steve Zdancewic
Abstract
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.
Published
In
Philosophical Transactions of the Royal Society A,
Volume 375, issue 2104, 24 pages, October 2017.