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

Publications

Events

Vampire Developers Meeting
January 11-12, 2016

Faculty of Informatics, TU Wien,
Favoritenstrasse 9-11,
Vienna, Austria

Aim:
The meeting aims at discussing ongoing work and work-in-progress in the Vampire theorem prover. We will also discuss future work and related ideas.

The workshop will bring together the developers of the Vampire theorem prover.

Workshop Venue:
The workshop will take place at the Faculty of Informatics of the TU Wien. The exact address is Favoritenstrasse 9-11, 1040 Vienna, Austria.

Workshop Program:

    January 11, 2016 - seminar room von Neumann
    • 13:00 Talk of Ann-Christin Knoll
      master student with interest in joining the Vampire team in Vienna;
      she will describe her master thesis work on resolution theorem proving

    • 14:30 Talk by Bernhard Gleiss
      semester project presentation and master thesis proposal on interpolation, with relation to Vampire
    • 16:00 Talk by Evgeny Kotelnikov
      CPP'16 talk rehearsal, and discussion on FOOL and CNF transformation
    • 19:00 Dinner at Artner Restaurant - Wieden, Floragasse 6, 1040 Vienna
    January 12, 2016 - seminar room Menger
    • 10:00-12:00: Talk by Simon Robillard
      Reasoning about inductive data types in Vampire
    • 12:00-14:00: Lunch at Restaurant Manzana, Apfelgasse 1, 1040 Vienna
    • 14:00-17:00: New features, work in progress in Vampire
      Giles Reger, Martin Suda, Andrei Voronkov: Vampire development, AVATAR, SMT/TPTP
      Laura Kovács, Max Jaroschek: (Polynomial) arithmetic, program analysis
      anything else related
    • 17:00-18:00: RiSE Seminar Talk by Martin Suda