Schedule
Click here for the List of Talks, with abstracts and links to papers and slides.
Click here to return to Workshop Homepage.
| 09:00 | Arrival | ||
| 09:15 | Workshop Start | ||
| 09:15-10:20 | Session 1 | Opening and Keynote Chair: Vijay Ganesh | |
| 09:15-09:20 | Opening Remarks | ||
| 09:20-10:20 | Jeremy Avigad | The Lean Theorem Prover | |
| 10:20-10:45 | Break (25min) | ||
| 10:45-12:20 | Session 2 | Symbolic developments in SMT and mathematics applications Chair: Matthew England | |
| 10:45-11:05 | Tarik Viehmann, Gereon Kremer and Erika Ábrahám | Comparing Different Projection Operators in the Cylindrical Algebraic Decomposition for SMT Solving | |
| 11:10-11:30 | Erika Abraham, Jasper Nalbach and Gereon Kremer | Embedding the Virtual Substitution Method in the Model Constructing Satisfiability Calculus Framework | |
| 11:35-11:55 | Rui-Juan Jing and Marc Moreno Maza | Computing the Integer Points of a Polyhedron | |
| 12:00-12:20 | Curtis Bright, Ilias Kotsireas and Vijay Ganesh | A SAT+CAS Method for Enumerating Williamson Matrices of Even Order | |
| 12:20-13:40 | Lunch (1hr 20min) | In Sommerhause (location 7 on Campus Map) | |
| 13:40-14:50 | Session 3 | Progress in traditional SAT applications from SC2 approaches Chair: Erika Abraham | |
| 13:40-14:00 | Daniela Ritirc, Armin Biere and Manuel Kauers | Complexity of circuit ideal membership testing | |
| 14:05-14:25 | Maximilian Jaroschek, Andreas Humenberger and Laura Kovács | Polynomial Invariant Generation for Multi-Path Loops | |
| 14:30-14:50 | Deepak Kapur | Nonlinear Polynomials, Interpolants and Invariant Generation for System Analysis | |
| 14:50-15:15 | Break (25min) | ||
| 15:15-16:25 | Session 4 | New theoretical breakthroughs Chair: James H. Davenport | |
| 15:15-15:35 | Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm and Xuan Tung Vu | Subtropical Satisfiability | |
| 15:40-16:00 | Jan Horacek and Martin Kreuzer | On Conversions from CNF to ANF | |
| 16:05-16:25 | Martin Bromberger and Christoph Weidenbach | Computing a Complete Basis for Equalities Implied by a System of LRA Constraints | |
| 16:25-16:50 | Break (25min) | ||
| 16:50-18:00 | Session 5 | SAT developments in Computer Algebra Systems Chair: Pascal Fontaine | |
| 16:50-17:10 | John Abbott and Anna Maria Bigatti | New in CoCoA-5.2.0 and CoCoALib-0.99550 for SC-SQUARE | |
| 17:15-17:35 | Martin Brain, James H. Davenport and Alberto Griggio | Benchmarking Solvers, SAT-style | |
| 17:40-18:00 | Stephen Forrest | Integration of SMT-LIB support into Maple | |
| 18:00 | Workshop End | ||
| 18:30 | Dinner | In Unique (location 27 on Campus Map) | |