Abstracts of the keynotes or techical presentations can be found here
or here, respectively.
January 31, 2017
| 15:00 – 17:00
| Welcome Reception
|
Session 1 (chair: Georg Moser)
| 17:00 – 17:10
| Opening
|
| 17:10 – 17:30
| Cezary Kaliszyk
|
| Proof Assistant Advice for Multiple Logical Foundations
|
| 17:30 – 17:50
| Kenji Miyamoto
|
| Implementing the Embedding Lemma
|
| 17:50 – 18:10
| Sarah Winkler
|
| Ground Confluence and Maximal Ordered Completion
|
| 18:10 – 18:30
| Martin Avanzini
|
| Complexity Analysis of Functional Programs via Sized-types
|
February 1, 2017
Keynote 1 (chair: Thomas Eiter)
| 08:00 – 09:00
| Moshe Vardi
|
| The Automated-Reasoning Revolution: From Theory to Practice and Back
|
Session 2 (chair: Kenji Miyamoto)
| 09:00 – 09:20
| Matthias Baaz
|
| LKepsilon and the immedeate reduction of arbitrary cuts to universal cuts
|
| 09:20 – 09:40
| Norbert Preining
|
| Classification of SAT and VAL in Gödel Logics
|
| 09:40 – 10:00
| Stefan Hetzl
|
| System Description: General Architecture for Proof Theory (GAPT)
|
| 10:00 – 14:00
| Coffee Break → Wintry Activities
|
Session 3 (chair: Martin Avanzini)
| 14:20 – 14:40
| Christoph Kirsch
|
| Teaching Computer Science Through Self-Referentiality
|
| 14:40 – 15:00
| Ana Sokolova
|
| Local Linearizability
|
| 15:00 – 15:20
| Petr Novotny
|
| Stochastic Invariants for Probabilistic Termination
|
| 15:20 – 15:40
| Mirco Giacobbe
|
| Counterexample-guided Refinement of Template Polyhedra
|
| 15:40 – 16:00
| Radu Grosu
|
| Temporal Logic as Filtering
|
| 16:00 – 16:30
| Coffee Break
|
Session 4 (chair: Sarah Winkler)
| 16:30 – 16:50
| Alexander Leitsch
|
| CERES in intuitionistic logic
|
| 16:50 – 17:10
| Anela Lolic
|
| Propositional interpolation induces first-order interpolation for finitely-valued logics
|
| 17:10 – 17:30
| Temur Kutsia
|
| A unification-Based Approach to the Construction of Orthogonal Designs in Powers of Two
|
| 17:30 – 17:50
| Thomas Eiter
|
| Streaming Multi-Context Systems
|
Business Meeting
| 18:00 – 18:30
| Discussion: Has HVW a Future?
|
Workshop Dinner
| 20:00 – 22:00
| University Centre
|
February 2, 2017
Keynote 2 (chair: Matthias Baaz)
| 08:00 – 09:00
| Erich Grädel
|
| The State of the Art in the Quest for a Logic for Polynomial Time
|
Session 5 (chair: Reinhard Pichler)
| 09:00 – 09:20
| Igor Konnov
|
| Verifying Safety and Liveness of Threshold-guarded Fault-Tolerant
Distributed Algorithms
|
| 09:20 – 09:40
| Georg Weissenbacher
|
| Accelerating Bug Detection in C Programs
|
| 09:40 – 10:00
| Georg Moser
|
| Multivariate Amortised Resource Analysis for Term Rewrite Systems
|
| 10:00 – 14:00
| Coffee Break → Wintry Activities
|
Session 6 (chair: Georg Weissenbacher)
| 14:00 – 14:20
| Martina Seidl
|
| QRAT Proofs for QBF Preprocessing
|
| 14:20 – 14:40
| Uwe Egly
|
| Quantifier Handling in QBF Calculi
|
| 14:40 – 15:00
| Reinhard Pichler
|
| CSPs and CQs: the Hardness of Identifying Easy to Solve Cases
|
| 15:00 – 15:20
| Michael Morak
|
| The Power of Non-Ground Rules in Answer Set Programming
|
| 15:20 – 15:40
| René Thiemann
|
| Certifying Termination Proofs for Programs
|
| 15:40 – 16:15
| Coffe Break and Closing
|
| 16:15
| Shuttle leaves for Innsbruck Main Station
|