[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
Applications are now invited for participation in the
Third DeepSpec Summer School (DSSS'20)
New Haven, CT, July 13-24, 2020
https://deepspec.org/event/dsss20
Overview
--------
Can critical systems be built according to functionally precise
specifications of of their constituent components (processor,
operating system, crypto library,..) and development tools (compilers,
synthesis tools)? This may seem a pipe dream, but the past decade has
seen remarkable advances in the technology required to realize it. The
DeepSpec summer school will provide students with knowledge and
experience necessary for understanding the state of the art and for
contributing to ongoing research efforts, based on the interactive
proof assistant Coq. The school is supported by generous funding from
the National Science Foundation.
DSSS'20 will consist of two parts with the first week being devoted to
introductory topics and the second week covering current research
efforts.
July 13-15 (Mon-Wed) Coq intensive; CertiKOS design & spec
July 16-17 (Thu-Fri) Fundamental proof techniques and project overviews
July 20-24 (week 2) Advanced topics in system verification
- Week 1 begins with a Coq Intensive, introducing our favorite proof
assistant (used in almost all other lectures), with no assumption of
formal-methods experience. A mix of lecturers (who will also
present research lectures later in the program) will cover this
material.
- For participants who already know the Coq Intensive material, we
will offer a Week 1 parallel track taught by Zhong Shao, on the
CertiKOS operating-system framework, focused on the compositional
specification and implementation of C modules, setting up to learn
how to prove these modules in Week 2.
- Week 1 ends with lectures by Andrew Appel, on verified functional
algorithms; and Joe Tassarotti, on theory and computer-systems
applications of the Iris verification framework for concurrency.
- Week 2 includes lectures by Adam Chlipala, on connecting proofs of
hardware and software components for embedded systems; Benjamin
Pierce, on random testing and an application to web servers; Zhong
Shao, on operating-system verification; Matthieu Sozeau, on the
MetaCoq framework and (as a representative of the Coq team at Inria)
recent improvements in and latest roadmap for Coq; Stephanie
Weirich, on verifying functional algorithms written in Haskell; and
Steve Zdancewic, on the Interaction Trees formalism and its
applications to compilers and testing.
- There will be ample opportunity for self-study/homework, student
presentations, and other activities.
Prerequisites
-------------
DSSS'20 is aimed at a wide range of participants, including graduate
students, academics, and industrial engineers and researchers.
The Coq proof assistant will serve as a lingua franca for all the
lectures. Participants who are not familiar with Coq at the level of
Software Foundations (Volume 1) should plan on attending the Coq
Intensive. Participants unfamiliar with volumes 2 and 3 may benefit
from attending the last 3 days of week 1.
Participants of DSSS'17 and DSSS'18 are likely to be admitted for
participation in week 2 only.
Application and participation
-----------------------------
Participation in DSSS'20 is by invitation only, based on an
application process that is open to anybody. To apply, please fill
this application form
https://cvent.me/xqlq0G
preferably no later than March 27, 2020. Accepted participants will be
notified shortly thereafter, and will be invited to confirm their
participation by registering.
Thanks to the generosity of NSF, we will be able to provide
substantial financial assistance to all participants. We will not
charge a registration fee, and will offer free dorm accommodation on
the campus of Yale University. In addition, we expect to
subsidize travel expenses for the majority of participants, based on
their geographic origin, qualification, and financial needs. To help
us allocating these funds, the application form includes the option to
enter estimated travel costs etc.
Late applications will be handled on a case-by-case basis.
For additional information on the DeepSpec project, please see
https://deepspec.org
