SUMo'2011 + Componet 2011 International Workshop on Scalable and Usable Model Checking for Petri Nets and other models of Concurrency

Preliminaries

This workshop was intended to be located at Kanazawa, together with PETRI NETS & ACSD 2011. Unfortunately, events changed these plans. On behalf of all SUMo organizers, we would like to express our deepest sympathy and send words of support and hope to people in Japan, including many personal friends and colleagues.

The workshop will be relocated, together with PETRI NETS & ACSD 2011 in Newcastle, UK (same period). To integrate all these changes, the deadline for submission is pushed to April 17, 2011. This year, the workshops SUMo and Componet have merged together to brought a consistent and stronger program.

Scope and Aims

This workshop is organized as a satellite event of the 32nd International Conference on Petri Nets and other models of concurrency (PETRI NETS 2011) and the 11th International Conference on Application of Concurrency to System Design (ACSD 2011).

The emergence of new efficient techniques for model checking makes possible the application of verification techniques to industrial-size specifications. This workshop is also interested in abstraction techniques since they are also another way to tackle this problem.

The purpose of SUMO'2011 is to create a forum in order to discuss new techniques and algorithms for model checking with a focus on their actual implementation in dedicated tools that cope with combinatorial explosion. This is the second edition of this workshop (see here for the first edition).

Model Checking Contest

Reference benchmarks derived from known cases studies and industrial applications will be proposed. The contest will be organized to compare performance of existing techniques and put an emphasis on tools with regards to their performances (time, memory consumption). Benchmarks will focus on various aspects of model checking (explicit, symbolic, use of symmetries, etc.). Details on the tool submission process will be announced later on the web site in the dedicated section.

PhD Forum

PhD students are encouraged to present their current work, they will be invited in a dedicated session. The session is mainly meant for PhD Students in the first half of their PhD project that have a well defined problem statement and some ideas about the solution that they want to discuss with. Each submitted paper will be reviewed by SUMo PC members who will provide feedback on their plans and suggest future directions.

Invited speaker

to be announced.

Topics

Topics include (but are not limited to) the following:

  1. PuceDecision diagram based techniques,

  2. PuceSymmetry-based techniques,

  3. PuceTechniques for infinite systems,

  4. PuceTechniques for timed and stochastic systems,

  5. PuceSAT-based techniques,

  6. PuceProperty-driven optimization,

  7. PuceArchitectures for efficient model checking tools,

  8. PuceParallel algorithms for model checking,

  9. PuceAbstract interpretation techniques,

  10. PuceAbstractions for handling underspecified systems,

  11. PucePattern-based abstractions,

  12. PuceAbstraction for efficiency, explanation, anytime reasoning,

  13. PuceMethodologies for applying abstraction techniques in modelling,

  14. PuceCase studies where abstraction plays a central role,

  15. Puceetc.

Extended versions of the best accepted papers will be invited for publication in the "Transactions on Petri Nets and Other Models of Concurrency" (TOPNoC) journal subline of Lecture Notes in Computer Science.

A satellite event of PETRI NETS'2011 and ACSD'2011

June  21, 2011