| Cover |
|
| Title pages, preface and table of contents |
iii |
Using unfoldings in automated testing of multithreaded programs
Keijo Heljanko |
1 |
Relating computational effects by TT-lifting
Shin-ya Katsumata |
2 |
Multi-core model checking for biological applications
Jaco van de Pol |
3 |
Productive infinite objects via copatterns
Andreas Abel |
4 |
Behavioral comparison of acyclic business process models
Abel Armas-Cervantes, Paolo Baldan and Luciano Garcìa-Bañuelos |
7 |
Translating a modeling and simulation language to hybrid automata
Kevin Atkinson, Adam Duracz and Walid Taha |
10 |
Input-output conformance testing of software product lines
Harsh Beohar and Mohammadreza Mousavi |
13 |
Formalizing a system for deadlock checking by data race detection in Coq
Peter Brottveit Bock |
16 |
Inheritance is subtyping
Robert Cartwright and Moez Abdel-Gawad |
19 |
The delay monad and restriction categories
James Chapman, Tarmo Uustalu and Niccolò Veltri |
22 |
A comparison of runtime assertion checking and theorem proving for concurrent and distributed systems
Crystal Chang Din, Richard Bubel and Olaf Owe |
25 |
Towards practical verification of dynamically typed programs
Björn Engelmann |
28 |
Certified normalization of context-free grammars
Denis Firsov and Tarmo Uustalu |
31 |
Extending abstract behavioral specifications with Erlang-style error handling
Georg Göri, Bernhard K. Aichernig, Einar Broch Johnsen, Rudolf Schlatte and Volker Stolz |
34 |
Towards a core language for separate variability modeling
Alexandru Florin Iosif-Lazar, Ina Schaefer and Andrzej Wasowski |
37 |
A categorical foundation of functional reactive programming with mutable state
Wolfgang Jeltsch |
40 |
On exploiting progress for memory-efficient verification of diagrammatic workflows
Lars Michael Kristensen, Yngve Lamo, Wendy MacCaull, Fazle Rabbi and Adrian Rutle |
43 |
The advantage of using co-span graph transformations for meta-model evolution
Florian Mantz and Uwe Wolter |
46 |
Synchronization property checking and inference in a lock-step synchronous parallel Replica language
Jari-Matti Mäkelä, Ville Leppänen and Martti Forsell |
50 |
Event structures as psi-calculus
Håkon Normann |
53 |
ST-configuration structures
Cristian Prisacariu |
56 |
Lock-polymorphic behaviour inference for deadlock checking
Ka I Pun, Martin Steffen and Volker Stolz |
60 |
Structural congruences for bialgebraic semantics
Jurriaan Rot and Marcello Bonsangue |
64 |
LCT-D: proof guided tests for C programs on LLVM
Olli Ilari Saarikivi and Keijo Heljanko |
67 |
Modelling critical systems with time constraints in Event-B
Faezeh Siavashi, Marina Waldén, Leonidas Tsiopoulos and Jüri Vain |
70 |
Verification of graph-based model transformations using Alloy
Xiaoliang Wang and Yngve Lamo |
73 |