Date: | Mon, 19 Mar 2018 11:03:41 -0500 |
---|---|
From: | "Loris D'Antoni" <loris@xxxxxxxxxxx> |
Subject: | [pl-seminar] Pretty cool summer school |
This seems like a very nice summer school.
Also, I found the summer schools I attended during my phd to be very useful for my career. Met many future colleagues (e.g., Aws) and learned fun stuff. -Loris ---------- Forwarded message ---------- From:ÂN ShankarÂ<summerformalschool@xxxxxxxxx> Date: Mon, Mar 19, 2018 at 3:09 AM Subject: Eighth Summer School on Formal Techniques, Atherton California, May 19-25, 2018 To: N Shankar <summerformalschool@xxxxxxxxx>  Eighth Summer School on Formal Techniques,ÂMay 19 - May 25, 2018  Menlo College  Atherton, California ÂÂhttp://fm.csl.sri.com/SSFT18 Techniques based on formal logic, such as model checking, satisfiability, static analysis, and automated theorem proving, are finding a broad range of applications in modeling, analysis, verification, and synthesis. This school, the sixth in the series, will focus on the principles and practice of formal techniques, with a strong emphasis on the hands-on use and development of this technology. It primarily targets graduate students and young researchers who are interested in studying and using formal techniques in their research. A prior background in formal methods is helpful but not required. Participants at the school can expect to have a seriously fun time experimenting with the tools and techniques presented in the lectures during laboratory sessions. The lecturers at the school include: * Emina Torlak (University of Washington)  Solver-Aided Programming  Abstract: Solver-aided tools have automated the verification and  synthesis of practical programs in many domains, from  high-performance computing to executable biology. These tools work  by reducing verification and synthesis tasks to satisfiability  queries, which involves compiling (bounded) programs to logical  constraints. The first lecture will cover the basics of symbolic  compilation for (bounded) program verification and synthesis. The  second lecture will cover an advanced, and rapid, way to construct  solver-aided tools by embedding them in Rosette, a solver-aided  programming language. Since its release in 2014, Rosette has enabled  a wide range of programmers, from professional developers to high  school students, to quickly create a variety of practical  solver-aided tools, from a verifier for radiation therapy software  to a synthesizer for algebra tutoring rules. The lab sessions will  use Rosette to demonstrate key ideas behind symbolic compilation and  solver-aided programming.  * Mooly Sagiv (Tel Aviv University)  Modularity for Decidability: Implementing and Semi-Automatically  Verifying Distributed Systems  Abstract: Proof automation can substantially increase productivity  in the formal verification of complex systems. However, the  unpredictablility of automated provers in handling quantified  formulas presents a major hurdle to usability of these tools. Here,  we propose to solve this problem not by improving the provers, but  by using a modular proof methodology that allows us to produce  decidable verification conditions. Decidability greatly improves the  predictability of proof automation, resulting in a more practical  verification approach. We apply this methodology to develop verified  implementations of distributed protocols with competitive  performance, showing its effectiveness.  This is a joint work with Marcelo Taube (TAU), Giuliano Losa(UCLA),  Ken McMillan (Microsoft Research), Oded Padon and Sharon  Shoham(TAU). The techniques have been implemented in IVY ÂÂÂhttps://www.microsoft.com/en-u * Nikhil Swamy and Jonathan Protzenko (Microsoft Research)  Programming and Proving in F* and Low*  Abstract: F* is an ML-like programming language aimed at program  verification. At its core is a type system based on dependent types,  refinement types and Hoare-style logics for user-defined monadic  effects. Together, these features allow expressing precise and  compact specifications for programs, including functional  correctness and security properties. The F* type-checker aims to  prove that programs meet their specifications using a combination of  SMT solving, user provided proof terms, as well as interactive  proofs using tactics.  This tutorial provides a general introduction to F* followed by a  focus on Low*, a subset of F* that extracts to C code for efficient,  low-level programming. The examples we present are drawn from  Project Everest, an ongoing effort using F* and Low* to verify and  deploy secure components in the HTTPS ecosystem, including protocols  such TLS and the cryptographic algorithms that underlie it. * Andreas Abel (Chalmers/Gothenburg University)  Introduction to Dependent Types and Agda  Abstract: Dependent types integrate programming with rich types,  specifications, and verification into a single language. Dependent  types allow to express arbitrary logical properties of programs, and  correctness proofs can be woven into the code.  In this tutorial, I will give a brief introduction to dependent  types and the dependently-typed language Agda developed at Chalmers.  We will understand the theoretical concepts as we walk through some  representative use cases. In the first part, we will learn how to  elegantly represent binary search trees and their ordering invariant  in Agda. In the second part, we will look at examples from  programming language, like representation of expressions,  evaluation, and equational reasoning. The tutorial is accompanied  by Agda programming and reasoning exercises. * Dirk Beyer (Ludwig Maximilian University, Munich, Germany)  Software Model Checking The main lectures in the summer school will be preceded by a background course on logic on * Natarajan Shankar (SRI CSL) and Stephane Graham-Lengrand (Ecole  Polytechnique) Speaking Logic  Abstract: Formal logic has become the lingua franca of computing. It  is used for specifying digital systems, annotating programs with  assertions, defining the semantics of programming languages, and  proving or refuting claims about software or hardware  systems. Familiarity with the language and methods of logic is a  foundation for research into formal aspects of computing. This course  covers the basics of logic focusing on the use of logic as a medium  for formalization and proof. We will also have invited talks by * Nina Narodytska (VMWare Research)  Verifying Properties of Binarized Deep Neural Networks * Gordon Plotkin (U. Edinburgh, UK)  Some Principles of Differentiable Programming Languages Research Papers * Edward A. Lee (UC Berkeley)  Plato and the Nerd - The Creative Partnership of Humans and Technology Information about previous Summer Schools on Formal Techniques can be found at http://fm.csl.sri.com/SSFT11 http://fm.csl.sri.com/SSFT12 http://fm.csl.sri.com/SSFT13 http://fm.csl.sri.com/SSFT14 http://fm.csl.sri.com/SSFT15 http://fm.csl.sri.com/SSFT16 http://fm.csl.sri.com/SSFT17 We expect to provide support for the travel and accommodation for (a limited number of) students registered at US universities. We welcome applications from non-US students as well as non-students (if space permits). Non-US students will have to cover their own travel and will be charged around US$800 for meals and lodging. Applications should be submitted at the websiteÂhttp://fm.csl.sri.com/SSFT18 Applicants are urged to submit their applications beforeÂApril 30, 2018, since there are only a limited number of spaces available. Non-US applicants requiring US visas are requested to apply early. We strongly encourage the participation of women and under-represented minorities in the summer school. |
[← Prev in Thread] | Current Thread | [Next in Thread→] |
---|---|---|
|
Previous by Date: | Re: [pl-seminar] Xbox Picture, Loris D'Antoni |
---|---|
Next by Date: | Re: [pl-seminar] Pretty cool summer school, Stephen Lee |
Previous by Thread: | [pl-seminar] Practice talks Monday (12/17), Calvin Smith |
Next by Thread: | Re: [pl-seminar] Pretty cool summer school, Stephen Lee |
Indexes: | [Date] [Thread] |