Wallenberg Academy Fellowsip 2014

TheProSE: Theorem Proving and Symbol Elimination
for Software Analysis and Verification

Principal Investigator: Laura Kovács
Funding Agency: Knut and Alice Wallenberg Foundation
Project Period: July 2015 - June 2020
Host Institution: Chalmers University of Technology

Project members


WAIT Workshop:
The Third Workshop on Automated Inductive Theorem-Proving
November 17-18, 2016

Seminar room Zemanek,
Vienna University of Technology,
Favoritenstrasse 9-11, Building (Stiege) 3, Ground floor
1040 Vienna, Austria

Inductive theorem proving is a topic of growing interest in the automated reasoning community. The Third Workshop on Automated Inductive Theorem-Proving - 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:30-15:00: Coffee Break
    • 15:00-16: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:30-16:45: Short Break
    • 16:45-17: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:00-10:00: Induction and Applications
      • Mathias Preiner: Quantified Bit Vectors and Synthesis
      • Tin Lok Wong: Model Theory of Arithmetic and Inductive Theorem Proving
    • 10:00-10:30: Coffee Break
    • 10:30-11:30: Discussion on Proof Formats for Inductive Proofs (discussion leaders: Moa Johansson, Evgeny Kotelnikov)
    • 11:30-12:00: Future of WAIT
    • 12:15-14:00: Buffet-Lunch at Wiener Wirtschaft,
                            Wiedner Hauptstr. 27-29, 1040 Vienna
    • 14:00-15:30: Theory Exploration and Conditionals
      • Moa Johansson: Hipster
      • Nick Smallbone: Conditional Laws in QuickSpec
      • Koen Claessen: TurboSpec
    • 15:30-16:00: Coffee Break
    • 16:00-17:00: Discussion on Benchmarking, Challenges (discussion leaders: Jasmin Blanchetter, Cezary Kaliszyk)

Workshop Organisers:


  • Alexander Bentkamp, Saarland University
  • Armin Biere, JKU Linz
  • Jasmin Blanchette, INRIA
  • Nicolas Braud-Santoni, 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

The workshop is partially supported by the ERC Starting Grant 2014 - SYMCAR 639270.