Program
All talks are held in Lindholmen Science Park, in the conference hall. The conference hall is in the building numbered 1 in the map found under Local info.
Day 1: Tuesday 8 Aug 2017
08:00 - 08:45 Registration
08:45 Conference Opening
09:00 - 10:00 Invited talk: Philippa Gardner
10:00 - 10:30 Coffee
10:30 - 12:00 Session 1: Theory combination
- Satisfiability Modulo Theories and Assignments. Maria Paola Bonacina, Stéphane Graham-Lengrand and Natarajan Shankar
- Notions of Knowledge in Combinations of Theories Sharing Constructors. Serdar Erbatur, Andrew M. Marshall and Christophe Ringeissen
- On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic. Marco Voigt, Christoph Weidenbach and Matthias Horbach
12:00 - 13:30 Lunch break
13:30 - 15:30 Session 2: Satisfiability
- [Best Paper] Short Proofs without New Variables. Marijn Heule, Benjamin Kiesl and Armin Biere
- Satisfiability Modulo Transcendental Functions via Incremental Linearization. Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri and Roberto Sebastiani
- Satisfiability Modulo Bounded Checking. Simon Cruanes
- Relational Constraint Solving in SMT. Baoluo Meng, Andrew Reynolds, Cesare Tinelli and Clark Barrett
15:30 - 16:00 Coffee
16:00 - 17:30 Session 3: Decision procedures
- Decision Procedures for Theories of Sets with Measures. Markus Bender and Viorica Sofronie-Stokkermans
- A Decision Procedure for Restricted Intensional Sets. Maximiliano Cristia and Gianfranco Rossi
- Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints. Andreas Teucke and Christoph Weidenbach
17:30 - 19:00 Reception by the City of Gothenburg (at the conference venue)
Day 2: Wednesday 9 Aug 2017
09:00 - 10:00 Invited EurAI talk: Grant Passmore
10:00 - 10:30 Coffee and start of CASC
10:30 - 12:00 Session 1: Proof certification
- Efficient Certified RAT Verification. Luís Cruz-Filipe, Marijn Heule, Warren Hunt, Matt Kaufmann and Peter Schneider-Kamp
- Efficient Verified (UN)SAT Certificate Checking. Peter Lammich
- Translating between implicit and explicit versions of proof. Roberto Blanco, Zakaria Chihani and Dale Miller
12:00 - 13:30 Lunch break
13:30 - 15:30 Session 2: First order logic
- [Best Paper] A Unifying Principle for Clause Elimination in First-Order Logic. Benjamin Kiesl and Martin Suda
- Splitting Proofs for Interpolation. Bernhard Gleiss, Laura Kovacs and Martin Suda
- Detecting Inconsistencies in Large First-Order Knowledge Bases. Stephan Schulz, Geoff Sutcliffe, Josef Urban and Adam Pease
- Theorem Proving for Metric Temporal Logic over the Naturals. Ullrich Hustadt, Ana Ozaki and Clare Dixon
15:30 - 16:00 Coffee
16:00 - 17:45 Session 3: System descriptions
- Scavenger 0.1: A Theorem Prover Based on Conflict Resolution. Bruno Woltzenlogel Paleo, Daniyar Itegulov and John Slaney
- WorkflowFM: A logic-based formal verification framework for process specification and composition. Petros Papapanagiotou and Jacques Fleuriot
- DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL. Florian Lonsing and Uwe Egly
- CSI: New Evidence - A Progress Report. Julian Nagele, Bertram Felgenhauer and Aart Middeldorp
- Scalable Fine-Grained Proofs for Formula Processing. Haniel Barbosa, Jasmin Christian Blanchette and Pascal Fontaine
Day 3: Thursday 10 Aug 2017
09:00 - 10:00 Invited talk: June Andronick
10:00 - 10:30 Coffee
10:30 - 12:00 Session 1: Confluence and termination
- Certifying Confluence of Quasi-Decreasing Strongly Deterministic Conditional Term Rewrite Systems. Christian Sternagel and Thomas Sternagel
- A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms. Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann and Daniel Wand
- Certifying Safety and Termination Proofs for Integer Transition Systems. Marc Brockschmidt, Sebastiaan Joosten, René Thiemann and Akihisa Yamada
12:00 - 13:30 Lunch break
13:00 - 14:30 Business Meeting
14:30 - Excursion
Day 4: Friday 11 Aug 2017
08:45 - 10:00 Best Paper Award, Skolem Award, Herbrand Award
10:00 - 10:30 Coffee
10:30 - 12:00 Session 1: Program verification
- Biabduction (and Related Problems) in Array Separation Logic. James Brotherston, Nikos Gorogiannis and Max Kanovich
- Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof. Gadi Tellez and James Brotherston
- Satisfiability of Compositional Separation Logic with Tree Predicates and Data Constraints. Zhaowei Xu, Taolue Chen and Zhilin Wu
12:00 - 13:30 Lunch break
13:30 - 15:30 Session 2: Applications and heuristics
- The binomial pricing model in finance: a formalization in Isabelle. Mnacho Echenim and Nicolas Peltier
- A Proof Strategy Language and Proof Script Generation for Isabelle/HOL. Yutaka Nagashima and Ramana Kumar
- Monte Carlo Tableau Proof Search. Michael Färber, Cezary Kaliszyk and Josef Urban
13:30 - 15:30 TPTP tea party (come to information desk at 13:20)
15:30 - Closing remarks