If you have any issues, please email Bernhard Beckert (beckert@kit.edu)

Programme

 6th MC and WG Meeting

Aalborg, Denmark • 26-28 January 2011

Aalborg University

For printing please use the print link in the footer of the page.

---

WEDNESDAY, January 26

9:00 - 9:05 Welcome

9:05 - 10:00 Adaptable and Reusable Programs (WG 1)

Ferruccio Damiani (with Ina Schaefer, Lorenzo Bettini)
Compositional Type-Checking for Delta-Oriented Programming

Vladimir Klebanov
Proof Reuse for Verification of Software Product Lines
(Report on STSM, 10min)

Discussion: Working Group 1
(Organised by Peter Schmitt. 15min)

10:00 - 10:30 Various Topics

Reiner Hähnle, Ran Ji, Richard Bubel
Implementing a Partial Evaluator via a Software Verification Tool

10:30 - 11:00 Coffee Break

11:00 - 12:30 Various Topics

Bent Thomsen
Trends in Programming

Davide Ancona
Coinductive Big-step Operational Semantics for Object-oriented Languages

Tarmo Uustalu (with Andri Saar)
Formal Reasoning about Software Transactions

12:30 - 13:00 Lunch Break

14:00 - 15:30 Evaluating Verification Systems

Vladimir Klebanov
The 1st Verified Software Competition

Benjamin Weiß
Applying the KeY System to the Problems from the 1st Verified Software Competition

Discussion on Evaluating Verification Systems
(Organised by Benjamin Weiß, Vladimir Klebanov)

15:30 - 16:00 Coffee Break

16:00 - 17:30 Management Committee Meeting

19:30 Dinner


THURSDAY, January 27

9:00 - 10:00 Invited Talk

Anders Ravn
Harnessing Theories for Real-Time Java Development

10:00 - 10:30 Concurrency, Mobility, Distributed Systems (WG 3)

Bogdan Tofan
Verifying a Lock-Free Stack with Hazard Pointers

10:30 - 11:00 Coffee Break

11:00 - 12:00 Concurrency, Mobility, Distributed Systems (WG 3)

Einar Broch Johnsen
Deployment Components with Parametric Concurrency

Discussion: Working Group 3
(Organised by Einar Broch Johnsen)

12:00 - 12:30 Modularisation and Components (WG 2)

Ioannis Kassios
Modular Specification and Verification of Delegation with SMT Solvers

12:30 - 14:00 Lunch Break

14:00 - 15:10 Modularisation and Components (WG 2)

Ilham Kurnia
Behavioral Composition of Object Group Components
(Work in progress, 20min)

Keiko Nakata
Securing Class Initialization

Discussion: Working Group 2
(Organised by Claude Marché, 20min)

15:10 - 15:40 Tool Integration (WG 4)

Joe Kiniry
tba

15:40 - 16:10 Coffee Break

16:10 - 17:40 Tool Integration (WG 4)

Mihai Balint
Automatic Model Field Inference Using Behavioral Subtyping

Daniel Bruns
A Complete Semantics of Model Fields

Discussion on Specification Languages
Is Specification the Bottle-neck of Program Verification? What is the Future of Specification Languages?
(Organised by Bernhard Beckert)


FRIDAY, January 28

9:00 - 9:30 Tool Demos / Teaching Formal Methods

Tool Demos

Short presentations on Teaching Formal Methods

9:30 - 10:30 Tool Integration (WG 4)

Frédéric Vogels
Annotation Inference for VeriFast
(15 min)

Gidon Ernst:
Verification of B+ Trees - An Experiment Combining Shape Analysis and Interactive Theorem Proving

Discussion WG 4
(Organised by Joe Kiniry, 15min)

10:30 - 11:00 Coffee Break

11:00 - 12:00 Testing and Fault Detection

Christoph Gladisch:
Software-fault Detection Based on Counterexamples of Verification Conditions

Amiram Yehudai:
Accelerating Test-Driven Development

12:00 - 12:30 Closing Discussion