Project members
Publications
Events

WAIT Workshop: The Third Workshop on Automated Inductive TheoremProving
November 1718, 2016
Seminar room Zemanek,
Vienna University of Technology,
Favoritenstrasse 911, Building (Stiege) 3, Ground floor
1040 Vienna, Austria
Aim:
Inductive theorem proving is a topic of growing interest in the automated reasoning community.
The Third Workshop on Automated Inductive TheoremProving  WAIT focuses on all relevant aspects of inductive reasoning.
The workshop is an informal event and aims to give researchers interested in the topic a chance to meet, exchange ideas and have an active platform for discussions.
We invite talks featuring demos and tutorials of inductive theorem provers, challenge problems, new directions of research or anything else of interest to the inductive theorem proving community.
Workshop Venue:
The workshop will take place at the Zemanek seminar room at the Faculty of Informatics of the Vienna University of Tehcnology.
Workshop Program:
Thursday, November 17
 14:3015:00: Coffee Break
 15:0016:30: Induction and Theorem Proving
 Simon Cuanes: Zipperposition  Induction in a Superposition Prover
 Simon Robillard: Term Algebras and Quantifiers
 Johannes Hoelzl: Automation in Isabelle's Analysis
 16:3016:45: Short Break
 16:4517:45: Inductive Reasoning about Programs
 Sebastian Zivota: Applying Loop Invariant Generation Techniques to Inductive Theorem Proving
 Nicolas Voirol: Theorem Proving on Programs
 19:00 : Workshop Dinner at Gasthaus Wolf,
Grosse Neugasse 20, 1040 Vienna
Friday, November 18
 9:0010:00: Induction and Applications
 Mathias Preiner: Quantified Bit Vectors and Synthesis
 Tin Lok Wong: Model Theory of Arithmetic and Inductive Theorem Proving
 10:0010:30: Coffee Break
 10:3011:30: Discussion on Proof Formats for Inductive Proofs
(discussion leaders: Moa Johansson, Evgeny Kotelnikov)
 11:3012:00: Future of WAIT
 12:1514:00: BuffetLunch at Wiener Wirtschaft,
Wiedner Hauptstr. 2729, 1040 Vienna
 14:0015:30: Theory Exploration and Conditionals
 Moa Johansson: Hipster
 Nick Smallbone: Conditional Laws in QuickSpec
 Koen Claessen: TurboSpec
 15:3016:00: Coffee Break
 16:0017:00: Discussion on Benchmarking, Challenges (discussion leaders: Jasmin Blanchetter, Cezary Kaliszyk)
Workshop Organisers:
Participants:
 Alexander Bentkamp, Saarland University
 Armin Biere, JKU Linz
 Jasmin Blanchette, INRIA
 Nicolas BraudSantoni, TU Graz
 Koen Claessen, Chalmers
 Simon Cruanes, INRIA
 Uwe Egly, TU Wien
 Katalin Fazekas, TU Wien
 Bernhard Gleiss, TU Wien
 Andreas Humenberger, TU Wien
 Maximillian Jaroschek, TU Wien
 Moa Johansson, Chalmers
 Stefan Hetzl, TU Wien
 Johannes Hoelzl, TU Muenchen
 Cezary Kaliszyk, Uni Innsbruck
 Jonatan Kilhamn, Chalmers
 Evgeny Kotelnikov, Chalmers
 Laura Kovacs, TU Wien
 Florian Lonsing, TU Wien
 Aina Niemetz, JKU Linz
 Mathias Preiner, JKU Linz
 Martin Riener, INRIA
 Simon Robillard, Chalmers
 Martina Seidl, JKU Linz
 Nick Smallbone, Chalmers
 Martin Suda, TU Wien
 Nicolas Voirol, EPFL
 Andrei Voronkov, U. Manchester and Chalmers
 Simon Wolfsteiner, TU Wien
 Tin Lok Wong, University of Vienna
 Sebastian Zivota, TU Wien
Acknowledgement:
The workshop is partially supported by the ERC Starting Grant 2014  SYMCAR 639270.
