Monday July 31 Tuesday August 1 Wednesday August 2 Thursday August 3 Friday August 4
08:00 Registration
08:45 Opening
09:00 State-of-the-art
SAT solving
slides (solving)code
Practical Session on
SAT/SMT
Symbolic Computation
(Quantifier Elimination)
Cylindrical Algebraic Decomposition
and Real Polynomial Constraints
slides
Industrial Applications and
Challenges for Verifying
Reactive Embedded Software
slides
10:30 Coffee break Coffee break Coffee break Coffee break Coffee break
11:00 State-of-the-art
SAT solving
slides (processing)
Practical Session on
SAT/SMT
Symbolic Computation
(Quantifier Elimination)
Cylindrical Algebraic Decomposition
and Real Polynomial Constraints
Formal Verification in
an Industrial Setting
slides (pdf) slides (mp4)
11:45 Closing
12:30 Lunch Lunch Lunch Lunch Lunch
14:00 Foundations of
Satisfiability Modulo Theories
slides
State-of-the-art
FOL Solving
slides
Syntax-Guided Synthesis
slides
Symbolic Computation through
Maple and Reduce
slides and worksheets
15:30 Coffee break Coffee break Coffee break Coffee break
16:00 Foundations of
Satisfiability Modulo Theories
Interactive Theorem Proving
in Higher-Order Logics
slides
Syntax-Guided Synthesis Symbolic Computation through
Maple and Reduce
17:30 Break
17:45 Formal Verification of
Financial Algorithms
Some information on Saarland,
its history, and the restaurant
18:00 Bus transfer to the restaurant
(from MPI)
18:30
19:00 Get together Dinner