Re: [pl-seminar] Pretty cool summer school

[Stephen Lee <snlee@xxxxxxxxxxx>]

Both Jason Breck and I also attended this and found it interesting.

Stephen

On 03/19/2018 11:03 AM, Loris D'Antoni wrote:

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-us/research/project/ivy/

*Â 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.

_______________________________________________
Pl-seminar mailing list
Pl-seminar@xxxxxxxxxxx
https://lists.cs.wisc.edu/mailman/listinfo/pl-seminar