Time | Speaker | Lecture | |||
---|---|---|---|---|---|
08:30-10:00 | Alexander Nadel | Introduction to SAT 1/2 | [slides] | ||
10:00-10:30 | (coffee break) | ||||
10:30-12:00 | Bruno Dutertre | Introduction to SMT 1/2 | [slides] | ||
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-17:00 | Marijn J.H. Heule | Proofs of Unsatisfiability: Validation and Applications | [slides] |
Time | Speaker | Lecture | |||
---|---|---|---|---|---|
08:30-10:00 | Alexander Nadel | Introduction to SAT 2/2 | [slides] | ||
10:00-10:30 | (coffee break) | ||||
10:30-12:00 | Bruno Dutertre | Introduction to SMT 2/2 | [slides] | ||
12:00-13:30 | (lunch) | ||||
13:30-15:00 | Dana Fisman | Introduction to Syntax-Guided Synthesis | [slides] | ||
15:00-15:30 | (coffee break) | ||||
15:30-17:00 | Yakir Vizel | Using SAT by-products in Model Checking | [slides] |
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 | [slides] | ||
12:00-13:30 | (lunch) | ||||
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:30 | (lunch) | ||||
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 | Constraint Minds Think Alike: The application of CP & SAT to Solve Hard Combinatorial Problems | [slides] | ||
17:00-17:15 | (coffee break) | ||||
17:15-17:45 | Certora (Yoav Rodeh) | Verifying smart contracts: SMT real life challenges and solutions | [slides] |