WING 2009

March 29, 2009

9:00 - 10:00: Keynote Speaker: Andrey Rybalchenko (MPI-SWS, Germany)

Improving Scalability of Invariant Generation for Assertion Checking

10:00-10:30: Bahareh Badban, Stefan Leue and Jan-Georg Smaus

Automated Invariant Generation for the Verification of Real-Time Systems

10:30-11:00: Tea/Coffee Break

11.00-11.30: Asma Louhichi, Olfa Mraihi, Lamia Labed and Ali Mili

Invariant Assertions, Invariant Relations, and Invariant Functions

11.30-12.00: Jan Olaf Blech, Thanh-Hung Nguyen and Michael Perin

Invariants and Robustness of BIP Models

12.00-12.30: Florin Craciun, Chenguang Luo, Guanhua He, Shengchao Qin and Wei-Ngan Chin

Discovering Specifications for Unknown Procedures - Work in Progress

12.30-14.00: Lunch

14.00-14.30: Gudmund Grov and Andrew Ireland

Towards Automated Property Discovery within Hume

14.30-15.00: Angela Wallenburg

Generalisation of Induction Formulae based on Proving by Symbolic Execution

15.00-15.30: Ewen Maclean, Andrew Ireland, Lucas Dixon and Robert Atkey

Refinement and Term Synthesis in Loop Invariant Generation

15.30-16.00: Tea/Coffee Break

16.00-17.00: Keynote Speaker: Leonardo de Moura (Microsoft Research, USA)

Applications and Challenges in Satisfiability Modulo Theories

17.00-18.00: Discussion: Challenges & Opportunities

18.00-18.15: Workshop Close