[DL] Tenth Summer School on Formal Techniques, May 16-22, 2020; First FMiTF Bootcamp, May 23-28, 2020, Atherton, California

Natarajan Shankar shankar at csl.sri.com
Thu Feb 27 01:00:00 CET 2020

Tenth Summer School on Formal Techniques , May 16 - May 22, 2020 
First Formal Methods in the Field (FMiTF) Bootcamp, May 23-28, 2020 
Menlo College, Atherton, California

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 tenth 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:

* Thomas Reps (University of Wisconsin)
   Algebraic Program Analysis: Automating Abstract Interpretation
* Pamela Zave (Princeton University)
   Specification, Implementation, and Verification of Network Properties
* J Strother Moore and Warren A. Hunt, Jr. (University of Texas)
   Proving Properties of Algorithms, Hardware, and Software with ACL2
* Jose Meseguer (University of Illinois at Urbana-Champaign)
   Executable Formal Specification and Verification in Maude

The main lectures in the summer school start on Monday May 18 and
  will be preceded by a background course on logic:
* Natarajan Shankar (SRI CSL) and Stephane Graham-Lengrand (Ecole 
   Speaking Logic
The summer school will be immediately followed by the
First Formal Methods in the Field (FMiTF) Bootcamp
May 23-28, 2020
Menlo College, Atherton, CA

The first FMitF Bootcamp will cover two themes, "Building Verified JIT
Compilers" and "Formally verifying low-level programs in F*". The
exercises in the Bootcamp assume that the students have a working
knowledge of formal techniques. The main focus of the Bootcamp is on
applying this knowledge to some domain-specific challenge problems.


  *  Emina Torlak and Xi Wang (University of Washington)
     Building Verified JIT Compilers

  * Jonathan Protzenko and Nikhil Swamy (Microsoft Research)
    Formally verifying low-level programs in F*
The summer school also include several distinguished invited talks.
Information about previous Summer Schools on Formal Techniques can be 
found at

Jay Bosamiya of CMU has blogged about the 2018 Summer School at
You are welcome to register for one or both of the summer school and
the Bootcamp.  The target audience for both events is
first/second/third year graduate students in computer science.  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 (who will be
admitted only if space permits).  Non-US students will have to cover
their own travel and will be charged around US$800 for the summer school
and $700 for the Bootcamp covering meals and lodging.  Applications 
should be
submitted at the website http://fm.csl.sri.com/SSFT20

Applicants are urged to submit their applications before April 30,
2020, 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.

More information about the dl mailing list