Accepted Papers

Marrying Words and Trees (invited talk)
Rajeev Alur

Simulation Using Orchestration (invited talk)
David Kitchin, Evan Powell, Jayadev Misra

Liberate Computer User from Programming (invited talk)
Teodor Rus

An Algebra for Features and Feature Composition
Sven Apel, Christian Lengauer, Bernhard Moeller, Christian Kaestner

Petri nets are dioids
Paolo Baldan, Fabio Gadducci

Towards an Efficient Implementation of Tree Automata Completion
Emilie Balland, Yohan Boichut, Pierre-Etienne Moreau, Thomas Genet

Calculating Invariants as Coreflexive Bisimulations
Luis Barbosa, Jose Oliveira, Alexandra Silva

Types and Deadlock Freedom in a Calculus of Services, Sessions and Pipelines
Roberto Bruni, Leonardo Gaetano Mezzina

A declarative debugger for Maude
Rafael Caballero, Narciso Marti-Oliet, Adrian Riesco, Alberto Verdejo

Long-Run Cost Analysis by Approximation of Linear Operators over Dioids
David Cachera, Thomas Jensen, Arnaud Jobin, Pascal Sotin

Towards Validating a Platoon of Cristal Vehicles using CSP||B
Samuel Colin, Arnaud Lanoix, Olga Kouchnarenko, Jeanine Souquieres

Explaining Verification Conditions
Ewen Denney, Bernd Fischer

Towards Formal Verification of ToolBus Scripts
Wan Fokkink, Paul Klint, Bert Lisser, Yaroslav S. Usenko

A Formal Analysis of Complex Type Flaw Attacks on Security Protocols
Han Gao, Chiara Bodei, Pierpaolo Degano

Abstract Interpretation Plugins for Type Systems
Tobias Gedell, Daniel Hedin

Separation Logic Contracts for a Java-like Language with Fork/Join
Christian Haack, Clement Hurlin

Towards a Model-theoretic Semantics for Contract-based Software Components
Rolf Hennicker, Michel Bidoit

Implementing a categorical information system
Michael Johnson, Robert Rosebrugh

Constant complements, reversibility and universal view updates
Michael Johnson, Robert Rosebrugh

Coinductive Properties of Causal Maps
Jiho Kim

Extending Timed Process Algebra with Discrete Stochastic Time
Jasen Markovski, Erik de Vink

Vx86: x86 Assembler Simulated in C Powered by Automated Theorem Proving
Stefan Maus, Michal Moskal, Wolfram Schulte

Evolving Specification Engineering
Dusko Pavlovic, Peter Pepper, Douglas Smith

Verification of Java Programs with Generics
Kurt Stenzel, Holger Grandy, Wolfgang Reif

Domain Axioms for a Family of Near-Semirings
Georg Struth, Jules Desharnais

Generating specialized rules and programs for demand-driven analysis
K. Tuncay Tekle, Katia Hristova, Yanhong A. Liu

Non expansive Epsilon-Bisimulations
Simone Tini

A Hybrid Approach for Safe Memory Management in C
Syrine Tlili, Zhenrong Yang, Hai Zhou Ling, Mourad Debbabi

Service Specification and Matchmaking using Description Logic: An Approach Based on Institutions
M. Birna van Riemsdijk, Rolf Hennicker, Martin Wirsing, Andreas Schroeder

System Demonstration of Spiral, Program Generator for High-Performance Libraries for Linear Transforms
Yevgen Voronenko, Franz Franchetti, Frederic de Mesmay, Markus Pueschel

The verification of the on-chip COMA cache coherence protocol
Duong Vu, Li Zhang, Chris Jesshope