Unbounded Allocation in Bounded Heaps.

Jurriaan Rot, Frank S. de Boer, Marcello M. Bonsangue

 1-16

On the Complexity of Adding Convergence.

Alex Klinkhamer, Ali Ebnenasir

 17-33

Deadlock Checking by Data Race Detection.

Ka I. Pun, Martin Steffen, Volker Stolz

 34-50

Delta Modeling and Model Checking of Product Families.

Hamideh Sabouri, Ramtin Khosravi

 51-65

Lending Petri Nets and Contracts.

Massimo Bartoletti, Tiziana Cimoli, G. Michele Pinna

 66-82

On Efficiency Preorders.

Manish Gaur, S. Arun-Kumar

 83-94

Compiling Cooperative Task Management to Continuations.

Keiko Nakata, Andri Saar

 95-110

Extending UPPAAL for the Modeling and Verification of Dynamic Real-Time Systems.

Abdeldjalil Boudjadar, Frits W. Vaandrager, Jean-Paul Bodeveix, Mamoun Filali

 111-132

Efficient Operational Semantics for for Verification of Temporal Properties.

Dimitris Vekris, Catalin Dima

 133-149

Interval Soundness of Resource-Constrained Workflow Nets: Decidability and Repair.

Elham Ramezani, Natalia Sidorova, Christian Stahl

 150-167

Statistical Model Checking of a Clock Synchronization Protocol for Sensor Networks.

Luca Battisti, Damiano Macedonio, Massimo Merro

 168-182

A New Representation of Two-Dimensional Patterns and Applications to Interactive Programming.

Iulia Teodora Banu-Demergian, Ciprian Paduraru, Gheorghe Stefanescu

 183-198

Push-Down Automata with Gap-Order Constraints.

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Giorgio Delzanno, Andreas Podelski

 199-216

Model Checking MANETs with Arbitrary Mobility.

Fatemeh Ghassemi, Saeide Ahmadi, Wan Fokkink, Ali Movaghar

 217-232

Validating SCTP Simultaneous Open Procedure.

Somsak Vanit-Anunchai

 233-249

Improving Time Bounded Reachability Computations in Interactive Markov Chains.

Hassan Hatefi, Holger Hermanns

 250-266

Checking Compatibility of Web Services Behaviorally.

Kais Klai, Hanen Ochi

 267-282