What we're about

Are you passionate about good design and specification? Excited by recent advances in programming languages and verification tools?

The science of deep specification (http://deepspec.org/) is the subject of a National Science Foundation initiative for cutting edge work on software and hardware specification that is both truly exact and implementation-independent.

"Deep" specification is semi-officially defined as
• rich (describing complex component behaviors in detail);
• two-sided (connected to both implementations and clients);
• formal (written in a mathematical notation with clear semantics to support tools such as type checkers, analysis and testing tools, automated or machine-assisted provers, and advanced IDEs); and
• live (connected via machine-checkable proofs to the implementation and client code).

Perhaps equally important, deep specification raises the level of abstraction of specifications, by applying concepts from software architecture. It is modular or layered, and aims at constructively defining not just an implementation but context-equivalent classes of implementations. According to the research overview (http://deepspec.org/research/), "the greatest pay-off will come in elucidating the conceptual basis of deep specifications as a technique for abstraction and modularity, with the potential for equal or greater practical benefit as from ideas like data abstraction."

The NSF DeepSpec initiative builds on and subsumes previous work on a comprehensive source-code-to-metal Verified Software Toolchain (http://vst.cs.princeton.edu/), which in turn builds on the Coq (https://coq.inria.fr/) proof assistant and the CompCert (http://compcert.inria.fr/) verified C compiler. It includes subprojects for certified compilation of dependently typed programs from Coq to CompCert C (http://deepspec.org/research/CertiCoq/); a Coq-based implementation of QuickCheck (http://deepspec.org/research/QuickChick/); a certified operating system kernel built from certified abstraction layers (http://flint.cs.yale.edu/certikos/); verified LLVM (http://www.cis.upenn.edu/~stevez/vellvm/) compiler tools; formal Haskell (http://deepspec.org/research/Haskell/#]) with compilation to LLVM; and a Coq-based extension of BlueSpec (http://deepspec.org/research/Kami/) for verified circuit design. Deep specification based courses on compilers and operating systems and an advanced course on system verification (http://deepspec.org/education/) inspired by Software Foundations (https://www.cis.upenn.edu/~bcpierce/sf/current/index.html) are also under development.

The Silicon Valley Deep Specification Meetup will discuss topics related to any and all parts of this and related work, especially potential for early practical applications.

Past events (22)

Formal Verification of Computer Programs: A Primer

Online event

Functional Algorithms Ch. 1

Santa Clara University Library

Software Foundations Ch. 7 Coq exercises

Room EC325, Bannan Engineering Building, Santa Clara University

Software Foundations Ch. 6 Coq exercises

Room EC325, Bannan Engineering Building, Santa Clara University

Photos (1)