[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
Applications are now invited for participation in the Second DeepSpec Summer School (DSSS'18) Princeton, NJ, July 16-27, 2018 https://deepspec.org/event/dsss18 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'18 will consist of two parts with the first week being devoted to introductory topics and the second week covering current research efforts. July 16-18 (Mon-Wed) Coq Intensive July 19-20 (Thu-Fri) Fundamental proof techniques and project overviews July 23-27 (week 2) Advanced topics in system verification Lecturers and Topics for week 2 ------------------------------- Andrew Appel and Verifiable C: a logic and toolset for Lennart Beringer proving C programs correct Adam Chlipala Implementing, specifying, verifying, and compiling hardware components with Kami Zach Tatlock Verifying distributed systems Benjamin Pierce Property-based random testing with QuickChick All DeepSpec PIs Towards the specification and verification of a web server Prerequisites ------------- DSSS'18 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 are likely to be admitted for participation in week 2 only. Application and participation ----------------------------- Participation in DSSS'18 is by invitation only, based on an application process that is open to anybody. To apply, please fill this application form https://www.regonline.com/builder/site/?eventid=2209458 preferably no later than March 23, 2018. 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 Princeton 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.