4th International Workshop on Invariant Generation
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 [pdf-abstract] |
10:50 | Invariant Stream Generators using Automatic Abstract Transformers
based on a Decidable Logic. Pierre-Loic Garoche,
Temesghen Kahsai and Cesare Tinelli [pdf-abstract] |
11:10 | Automated Theorem Discovery: a Case Study. Roy McCasland (ATX) |
11:40 | Inferring Loop Invariants Dynamically.
Juan Pablo Galeotti and Andreas Zeller [pdf-abstract] |
12:00 | lunch break |
13:30 | Prinsys - A Software Tool for the Synthesis of Probabilistic
Invariants. Friedrich Gretz, Joost-Pieter Katoen,
and Annabelle McIver
[pdf-abstract] |
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
[pdf-abstract] |
14:40 | Augmenting formal development with use case
reasoning. Alexei Iliasov [pdf-abstract] |
15:00 | coffee break |
15:30 | Invited Astrée tutorial: Abstract
Domains for Bit-Level Machine Integer and
Floating-point Operations. Antoine
Miné [pdf] |
16:30 | Faster Automatic Test Case Generation. Ott
Tinn
[pdf-abstract] |
16:50 | Conclusive Proofs of While Loops Using
Invariant Relations. Lamia Labed Jilani, Wided
Ghardallou, Ali Mili
[pdf-abstract] |
17:10 | Formal Characterization and Verification of
Loop Invariant Based on Finite
Difference. Mengjun Li
[pdf-abstract] |
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
Url: http://www.macs.hw.ac.uk/cs/techreps/doc0097.html