[hpc-announce] 2024 Summer School on Formal Techniques, Atherton, California (May 25-31, 2024) + Formal Methods in the Field Bootcamp (June 1/2, 2024)

[Natarajan Shankar]

Thirteenth Summer School on Formal Techniques,  May 25 - June 3, 2024 (http://fm.csl.sri.com/SSFT24)
                              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 thirteenth in the series, focuses 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 the laboratory sessions.  The main lectures run from Monday May 27 to Fri May 31. They are preceded by a background course "Speaking Logic" taught by Natarajan  Shankar and Stephane Graham-Lengrand (SRI CSL) on May 25/26.  The summer  school 
is immediately followed by a two-day Bootcamp to reinforce some of the  skills acquired during the school.  Participants in the Bootcamp work with  formal tools and techniques (including those taught in this and prior summer school editions) under the supervision of the Bootcamp faculty to create verified artifacts.

The lecturers at  the school include:  Josef Urban (CIIRC): Combining Machine Learning and Theorem Proving; Marsha Chechik (U. Toronto): Elicitation and Formal Reasoning about Normative Requirements;  Leonardo de Moura and David Thrane Christiansen:  The Lean 4 programming language and theorem prover;  Cesare Tinelli (U. Iowa):  Modeling and analyzing reactive systems with logic-based symbolic model checkers;  Armando Solar-Lezama (MIT):  Neurosymbolic Programming for better learning.  The program also includes invited talks from distinguished speakers (to be announced).

This year, the school/bootcamp will take place in a hybrid mode: the lectures and labs will be live-streamed and recorded. We strongly encourage in-person participation so that you can benefit from interactions outside the classroom. We have funding from NSF to cover transportation/food/lodging expenses for selected US-based students. Non-student and non-US in-person participants are expected to cover their own transportation and will be charged a fee (around $150/day) to cover the cost of food and lodging.

The registration link is at the URL: http://fm.csl.sri.com/SSFT24. Applications should be submitted together with names of two references (preferably  advisors, professors, or senior colleagues). Applicants are urged to submit their applications as early as possible (no later than April 30, 2024), since there are only a limited number of spaces available.  Those needing invitation letters for visa purposes are encouraged to complete their applications as early as possible.  We strongly  encourage the participation of women and under-represented minorities in the summer school.