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:
* 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 main lectures are preceded by a background course "Speaking Logic" taught by Natarajan Shankar and Stephane Graham-Lengrand (SRI).

In addition, we have distinguished invited talks, including one by Prof. David McQueen on "Types and programming language design, based on the SML and SMLNJ experience".