Schedule (Tentative)

Day 1 (Sunday, August 14)

   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]  


Day 2 (Monday, August 15)

   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]  


Day 3 (Tuesday, August 16)

   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]  


Day 4 (Wednesday, August 17)

   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]