COSMICAH 2005

First international workshop on the verification of COncurrent Systems with dynaMIC Allocated Heaps

COSMICAH 2005

July 10, 2005, Lisboa, Portugal (a satellite event of ICALP 2005)

Programme

Program Commitee

Cristiano Calcagno (Imperial College, London)
Dino Distefano (Queen Mary U, London, co-chair)
Peter Habermehl (Liafa, Paris 7 University)
Peter O'Hearn (Queen Mary U, London, chair)
Radu Iosif (Verimag, Grenoble, co-chair)
Yassine Lakhnech (Verimag, Grenoble)
Arend Rensink (Twente University, Enschede)
Robby (Kansas State University, Manhattan KS)
Eran Yahav (IBM Research, New York)

Invited Speaker

Andreas Podelski (Max-Planck-Institut für Informatik, Saarbruecken)

Important Dates

Regular paper submission: May 23th, 2005 (extended)
Abstract/statement submission: June 10th, 2005
Acceptance/rejection notification: June 17th, 2005
Final version: June 24th, 2005
Workshop: July 10, 2005

Call for Papers (txt, ps, pdf)

Contacts

Radu Iosif (Radu dot Iosif at imag dot fr)
Dino Distefano (ddino at dcs dot qmul dot ac dot uk)

The ongoing growth in complexity of concurrent embedded programs requires new techniques capable of predicting their runtime errors. One of the reasons this complexity arises is the use of dynamic memory allocation and of recursive data structures in a concurrent setting. This is the case of most object-oriented languages with support for multithreading, where communication between threads is performed via shared objects implementing various synchronization policies.

Over the past decade, new techniques for the analysis of object-based and object-oriented programs have emerged. These solutions stem from a wide range of domains such as static analysis, model checking, theorem proving and Hoare logic.

This workshop aims at bringing together researchers from different subdomains of formal verification that share interest in the analysis of dynamic memory programs. Topics of interest are, but are not limited to:

application of graph rewriting to the verification of object-based programs

logics for describing heap topologies and their evolutions

abstraction techniques for infinite-state systems with dynamic heaps

high-level specification of local behaviors (e.g, object protocols, separation logic)

comparisons between existing techniques and tools

test cases and experimental results

specification and analysis of security protocols

COSMICAH is an official Appsem II workshop. Members of Appsem can use Appsem money to travel to it.

Submissions

Authors are invited to submit papers presenting recent work in the areas relevant for the scope of COSMICAH. Contributions should not exceed 15 pages in LNCS style. Accepted papers will be published in informal proceedings (as technical report of Queen Mary University of London) and distributed to the participants at the workshop. Given the informal proceedings, submitting to COSMICAH does not preclude simultaneous or future submission of the paper to major conferences. In this sense COSMICAH represents for authors a great platform to present their work and receive feedback.

To increase interaction among the participants, COSMICAH includes a special 5 minutes madness session. Authors are invited to submit one page research abstracts/statement (on recent and/or ongoing work) for this session. Abstracts/statements will be considered on the bases of their originality and attractiveness to the scope of the workshop.

Papers and abstracts should be submitted electronically (in ps or pdf format), by email to: ddino [at] dcs.qmul.ac.uk. Please indicate the type of your submission (regular paper or abstract).