Click here for the List of Talks, with abstracts and links to papers and slides.

Click here to return to Workshop Homepage.

09:15Workshop Start  
09:15-10:20Session 1Opening and Keynote
Chair: Vijay Ganesh
 09:15-09:20Opening Remarks 
 09:20-10:20Jeremy AvigadThe Lean Theorem Prover
10:20-10:45Break (25min)  
10:45-12:20Session 2Symbolic developments in SMT and mathematics applications
Chair: Matthew England
 10:45-11:05Tarik Viehmann, Gereon Kremer and Erika ÁbrahámComparing Different Projection Operators in the Cylindrical Algebraic Decomposition for SMT Solving
 11:10-11:30Erika Abraham, Jasper Nalbach and Gereon KremerEmbedding the Virtual Substitution Method in the Model Constructing Satisfiability Calculus Framework
 11:35-11:55Rui-Juan Jing and Marc Moreno MazaComputing the Integer Points of a Polyhedron
 12:00-12:20Curtis Bright, Ilias Kotsireas and Vijay GaneshA SAT+CAS Method for Enumerating Williamson Matrices of Even Order
12:20-13:40Lunch (1hr 20min)In Sommerhause (location 7 on Campus Map)
13:40-14:50Session 3Progress in traditional SAT applications from SC2 approaches
Chair: Erika Abraham
 13:40-14:00Daniela Ritirc, Armin Biere and Manuel KauersComplexity of circuit ideal membership testing
 14:05-14:25Maximilian Jaroschek, Andreas Humenberger and Laura KovácsPolynomial Invariant Generation for Multi-Path Loops
 14:30-14:50Deepak KapurNonlinear Polynomials, Interpolants and Invariant Generation for System Analysis
14:50-15:15Break (25min)  
15:15-16:25Session 4New theoretical breakthroughs
Chair: James H. Davenport
 15:15-15:35Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm and Xuan Tung VuSubtropical Satisfiability
 15:40-16:00Jan Horacek and Martin KreuzerOn Conversions from CNF to ANF
 16:05-16:25Martin Bromberger and Christoph WeidenbachComputing a Complete Basis for Equalities Implied by a System of LRA Constraints
16:25-16:50Break (25min)  
16:50-18:00Session 5SAT developments in Computer Algebra Systems
Chair: Pascal Fontaine
 16:50-17:10John Abbott and Anna Maria BigattiNew in CoCoA-5.2.0 and CoCoALib-0.99550 for SC-SQUARE
 17:15-17:35Martin Brain, James H. Davenport and Alberto GriggioBenchmarking Solvers, SAT-style
 17:40-18:00Stephen ForrestIntegration of SMT-LIB support into Maple
18:00Workshop End  
18:30DinnerIn Unique (location 27 on Campus Map)