The workshop will be held on June 25-26, 2007, as a satellite workshop of Calculemus 2007, in the frame of the RISC Summer 2007 conference series.

WING 2007 Schedule

June 25th

11:30 - 12:30: Registration

12:30 - 14:30: Lunch Break

14:30 - 15:30: Invited Speaker: Deepak Kapur (University of New Mexico, USA)

15:30 - 16:00: Coffee Break

16:00 - 17:00: Session 1 (2 talks)

• Laura Kovács:
  Automated Polynomial Invariant Generation by Algebraic Techniques for Imperative Program Verification in Theorema


• Andrew Ireland:
  A Cooperative Approach to Loop Invariant Discovery for Pointer Programs

19:00 - Late: Workshop Dinner (Pöstlingberg - Schlössl Restaurant, Linz)
shuttle bus leaves at 17:30 from RISC

June 26th

9:30 - 10:30: Invited Speaker: Reiner Hähnle (Chalmers University of Technology, Göteborg, Sweden)

10:30 - 11:00: Coffee Break

11:00 - 12:30: Session 2 (3 talks)

• Stefan Kauer and Jürgen Winkler:
  Mechanical Generation of Invariants for FOR-Loops


• Ali Mili.
  Reflexive Transitive Loop Invariants: A Basis for Computing Loop Functions


• Vladimir Zakharov and Igor Konnov:
  An Invariant-based Approach to the Verification of Asynchronous Parameterized Networks

12:30 - 14:30: Lunch Break

14:30 - 15:30: Invited Speaker: Andrei Voronkov (Manchester University, UK)

15:30 - 16:00: Coffee Break

16:00 - 17:00: Session 3 (2 talks)

• Mikoláš Janota:
  Assertion-based Loop Invariant Generation


• Rustan Leino and Francesco Logozzo:
  Using Widenings to Infer Loop Invariants Inside an SMT Solver, or: A Theorem Prover as Abstract Domain

17:00 - 18:00: Discussions, Concluding remarks

18:30 - 20:00: Soccer Tournament (Hagenberg)

20:00 - Late: Grill Party (Hagenberg)

June 27th

12:00 - 13:30: Lunch Break

13:30 - 14:30: Invited Speaker: John Harrison (Intel Corporation, USA) - jointly held with Calculemus 2007

Page maintained by Laura Kovács