| Time | Speaker | Lecture | |||
|---|---|---|---|---|---|
| 08:30-10:00 | Alexander Nadel | Introduction to SAT 1/3 | [slides pptx] [slides pdf] | ||
| 10:00-10:30 | (coffee break) | ||||
| 10:30-12:00 | Bruno Dutertre | Introduction to SMT 1/3 | [slides pptx] [slides pdf] | ||
| 12:00-13:30 | (lunch) | ||||
| 13:30-15:00 | Dana Drachsler Cohen | Safety of Neural Networks | [slides] | ||
| 15:00-15:30 | (coffee break) | ||||
| 15:30-16:15 | Alexander Nadel | Introduction to SAT 2/3 | [slides pptx] [slides pdf] | ||
| 16:15-17:00 | Bruno Dutertre | Introduction to SMT 2/3 | [LRA example] |
| Time | Speaker | Lecture | |||
|---|---|---|---|---|---|
| 08:30-10:00 | Alexander Nadel | Introduction to SAT 3/3 | [slides pptx] [slides pdf] | ||
| 10:00-10:30 | (coffee break) | ||||
| 10:30-12:00 | Bruno Dutertre | Introduction to SMT 3/3 | [slides] | ||
| 12:00-13:30 | (lunch) | ||||
| 13:30-15:00 | Guy Katz | Safety of Neural Networks #2 | [slides 1 pptx] [slides 1 pdf] [slides 2 pptx] [slides 2 pdf] | ||
| 15:00-15:30 | (coffee break) | ||||
| 15:30-17:00 | Dana Fisman | Introduction to Syntax-Guided Synthesis | [slides] | ||
| 18:00-21:00 | Summer School Dinner | Shuttle at 18:00 from Technion |
Dinner will be held at the Leonardo Plaza Hotel in Haifa, at 18:30. A bus will leave from the Taub building at 18:00 - please be there on time. For those arriving independently, the address is David Elazar St 10, Haifa; here are links for Google Maps and Waze. The bus back to the Technion will leave the restaurant at 21:00.
| Time | Speaker | Lecture | |||
|---|---|---|---|---|---|
| 08:30-10:00 | Cezary Kaliszyk | Introduction to ITP 1/2 | [slides] | ||
| 10:00-10:30 | (coffee break) | ||||
| 10:30-12:00 | Cezary Kaliszyk | Introduction to ITP 2/2 | |||
| 12:00-13:00 | (lunch) | ||||
| 13:00-13:30 | Guided tour of the Technion CS building | ||||
| 13:30-15:00 | Shachar Itzhaky | Formal Software Verification in Proof Assistants | [slides] | ||
| 15:00-15:30 | (coffee break) | ||||
| 15:30-17:00 | Philipp Ruemmer | From Craig Interpolation for Theories to Horn Solving | [slides] |
| Time | Speaker | Lecture | |||
|---|---|---|---|---|---|
| 08:30-10:00 | George Katsirelos | Introduction to CP | [slides] | ||
| 10:00-10:30 | (coffee break) | ||||
| 10:30-12:00 | George Katsirelos | The cross-fertilization of CP and SAT | [slides] | ||
| 12:00-13:00 | (lunch) | ||||
| 13:00-13:30 | Certora (Yoav Rodeh) | Verifying smart contracts: SMT real life challenges and solutions | [slides] | ||
| 13:30-15:00 | Michael Veksler | Learning General Constraints in Hybrid CP/SAT Solvers | [slides] | ||
| 15:00-15:30 | (coffee break) | ||||
| 15:30-17:00 | Michael Codish | Breaking Symmetries when Solving Hard Combinatorial Problems | [slides] |