Program

PROGRAM

Days: Sunday, May 19th Monday, May 20th Tuesday, May 21st Wednesday, May 22nd Thursday, May 23rd

Sunday, May 19th

View this program: with abstracts session overview talk overview

14:00	Konstantin Korovin, Laura Kovacs and Giles Reger Opening, Welcome (abstract)
14:10	Andrei Voronkov Living with Vampire And Sleeping with EasyChair (abstract)

15:30-16:00Coffee Break

16:00-17:30 Session 2

16:00	Christoph Weidenbach Vampire-60: 1939 or 2045? (abstract)
16:40	Alexander Lyaletski Evidence Algorithm, SAD systems, and automated theorem proving (abstract)
17:00	Giles Reger How is Vampire doing? (abstract)

18:00-22:00Welcome Reception

Monday, May 20th

View this program: with abstracts session overview talk overview

09:00-10:30 Session 3: Invited Talks

Chair:

Laura Kovacs

09:00	Thomas Henzinger Temporal Logics for Multi-Agent Systems (abstract)
09:40	Nikolaj Bjorner Basic Hilbert Bases (abstract)
10:00	Temur Kutsia Anti-unification for lambda-terms: a generic approach (abstract)

10:30-11:00Coffee Break

11:00-12:30 Session 4: Invited Talks

11:00	Margus Veanes Some memories from mid-late 90s and how having Andrei as my PhD advisor impacted my life (abstract)
11:20	Arie Gurfinkel The Curse of Interpolation (abstract)
11:40	Jean-Pierre Jouannaud Rewrite Encodings in Dependent Type Theories: The Problem of Confluence (abstract)

12:30-14:00Lunch Break

14:00-15:30 Session 5: Invited Talks

14:00	Ruzica Piskac Using Hilbert Bases for Reasoning about Multisets (abstract)
14:40	Bertrand Meyer A Theory of Object Structures (abstract)

15:30-16:00Coffee Break

16:00-17:30 Session 6: Invited Talks

16:00	Franz Baader How to count chairs and bats in Description Logics (abstract)
16:20	Natasha Sharygina Interpolation infusion in SMT-based model checking (abstract)
17:00	Laura Kovacs 60 Shades of Grey in Vampire (abstract)

Tuesday, May 21st

View this program: with abstracts session overview talk overview

09:00-18:00 Excursion

Excursion

18:00-22:00Dinner

Wednesday, May 22nd

View this program: with abstracts session overview talk overview

10:00-10:30 Session 7: Invited Talks

Chair:

Martin Suda

10:00

Alexander Leitsch

Proof Schemata and Herbrand Systems (abstract)

10:30-11:00Coffee Break

11:00-12:30 Session 8: Invited Talks

Chair:

Martin Suda

11:00	Yuri Gurevich Witness algebra, or who needs category theory? (abstract)
11:40	Cesare Tinelli Counter-model-based quantifier Instantiation in SMT (abstract)

12:30-14:00Lunch Break

14:00-15:30 Session 9: Invited Talks

Chair:

Margus Veanes

14:00	Margarita Korovina Taylor Models for ERA (abstract)
14:20	Christoph Benzmüller Higher-order automated theorem proving -- Why has there been such a resistance? (abstract)
15:00	Martin Suda ENIGMA Given Clause Guidance (abstract)

15:30-16:00Coffee Break

16:00-17:30 Session 10: Invited Talks

Chair:

Margus Veanes

16:00	Michel Parigot Breaking the rules (abstract)
16:20	Konstantin Korovin Abstraction-refinement automated reasoning (abstract)
16:40	Geoff Sutcliffe Andrei ... Superman or Rocketman? (abstract)

Thursday, May 23rd

View this program: with abstracts session overview talk overview

10:00-10:30 Session 11: Invited Talks

Chair:

Nikolaj Bjorner

10:00

Aart Middeldorp

Projection Equivalence Revisited (abstract)

10:30-11:00Coffee Break

11:00-12:30 Session 12: Invited Talks

Chair:

Nikolaj Bjorner

11:00	Matthias Baaz Deskolemizing Andrew's Skolemization (abstract)
11:40	Nestan Tsiskaridze Conflict Resolution with WildCards (abstract)
12:00	Stephan Schulz Cooperation and Competition in Automated Theorem Proving (abstract)
12:20	Konstantin Korovin and Andrei Voronkov Closing (abstract)

12:30-13:15Lunch Break

17:00-18:30 Social Event

See the description on the social program page.

18:30-21:30 Closing Dinner

See the description on the social program page.