WING 2012

Invited Speakers

Preliminary Program

The program of WING 2012 will be joint with ATX 2012, which will continue on July 1. Contributions associated with ATX are marked accordingly.

09:00 Invited talk: Specification Inference and Invariant Generation: A Machine Learning Perspective. Aditya Nori
10:00 coffee break
10:30 SMT-Based Array Invariant Generation. Daniel Larraz, Enric Rodriguez-Carbonell, and Albert Rubio
10:50 Invariant Stream Generators using Automatic Abstract Transformers based on a Decidable Logic. Pierre-Loic Garoche, Temesghen Kahsai and Cesare Tinelli
11:10 Automated Theorem Discovery: a Case Study. Roy McCasland (ATX)
11:40 Inferring Loop Invariants Dynamically. Juan Pablo Galeotti and Andreas Zeller
12:00 lunch break
13:30 Prinsys - A Software Tool for the Synthesis of Probabilistic Invariants. Friedrich Gretz, Joost-Pieter Katoen, and Annabelle McIver
13:50 The Use of Rippling to Automate Event-B Invariant Preservation Proofs. Yuhui Lin, Alan Bundy and Gudmund Grov (ATX)
14:20 E-SPARK: Automated Generation of Verifiable Code from Formally Verified Designs. Rajiv Murali and Andrew Ireland
14:40 Augmenting formal development with use case reasoning. Alexei Iliasov
15:00 coffee break
15:30 Invited Astrée tutorial: Abstract Domains for Bit-Level Machine Integer and Floating-point Operations. Antoine Miné
16:30 Faster Automatic Test Case Generation. Ott Tinn
16:50 Conclusive Proofs of While Loops Using Invariant Relations. Lamia Labed Jilani, Wided Ghardallou, Ali Mili
17:10 Formal Characterization and Verification of Loop Invariant Based on Finite Difference. Mengjun Li
17:30 end of workshop

Technical Report

The contributions of the workshop are also available as a technical report:

Authors: Gudmund Grov and Thomas Wies (Eds)
Institution: Computer Science, School of Mathematical and Computer Science, Heriot-Watt University, UK
Report number: HW-MACS-TR-0097
Year: 2012