The school will cover several fundamental aspects of formal methods and applications:
- An Introduction to Learning from Programs, by Marc Brockschmidt
- Models and Techniques for Analyzing Security Protocols, by Veronique Cortier
- Neural Network Verification, by M. Pawan Kumar
- Computing with SAT Oracles: From CDCL SAT Solving to Ubiquitous Industry Adoption, by João Marques-Silva
- Abstract Interpretation, by Patrick Cousot. This tutorial will be complemented by an invited talk by Sylvie Putot (Ecole Polytechnique, France) on Zonotopic abstract domains for numerical program analysis.
- Developing distributed protocols formally with Ivy, by Ken McMillan This tutorial will be complemented by an invited talk by Kedar Namjoshi (Nokia Bell Labs,USA) on Modular Verification: Model Checking in Bits and Pieces.
Each topic will be covered through a long course of 3 hours.
Participants are expected to arrive on Tuesday evening and leave Saturday afternoon. Here is a tentative program (this will be finalized very soon):
Wednesday, January 9th:
09.00 – 12.30: Computing with SAT Oracles: From CDCL SAT Solving to Ubiquitous Industry Adoption (Joao Marques-Silva)
14.00 – 17.30: An Introduction to Learning from Programs (Marc Brockschmidt)
Thursday, January 10th:
09.00 – 12.30: Developing distributed protocols formally with Ivy (Ken McMillan)
14.00 – 17.30: Models and Techniques for Analyzing Security Protocols (Veronique Cortier)
Friday, January 11th:
09.00 – 12.30: Abstract interpretation (Patrick Cousot)
14.00 – 15.00: Zonotopic abstract domains for numerical program analysis (Sylvie Putot)
15.00 – 16.00: Modular Verification: Model Checking in Bits and Pieces (Kedar Namjoshi)
16.30 – 18.00: Panel discussion on the “Future of Formal Methods”. Moderator Lenore Zuck.
Saturday, January 12th:
09.00 – 12.30: Neural Network Verification (M. Pawan Kumar)