Model Checking of Concurrent Software Systems via Heuristic-Guided SAT Solving . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
Nils Timm, Stefan Gruner and Prince Sibanda
A Formal Model for Multi SPLs* . . . . . . . . . . . . . . . . . . . . . . . . ..16
Ferruccio Damiani, Michael Lienhardt and Luca Paolini
Translating Active Objects into Colored Petri Nets for Communication
Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
Anastasia Gkolfi, Crystal Chang Din, Einar Broch Johnsen, Martin
Steffen and Ingrid Chieh Yu
Composing families of Timed Automata . . . . . . . . . . . . . . . . . . .48
Guillermina Cledou, Jos´e Proen¸ca and Luis Barbosa
Debugging of Concurrent Systems using Counterexample Analysis. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .63
Gianluca Barbon, Vincent Leroy and Gwen Sala¨un
Synthesizing Parameterized Self-Stabilizing Rings With Constant-Space Processes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
Alex P. Klinkhamer and Ali Ebnenasir
Bisimilarity of Open Terms in Stream GSOS . . . . . . . . . . . . . . . 93
Filippo Bonchi, Matias David Lee and Jurriaan Rot
TCE+: an Extension of the TCE Method for Detecting Equivalent
Mutants in Java Programs . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109
Mahdi Houshmand and Samad Paydar
Using Swarm Intelligence to Generate Test Data for Covering Prime Paths . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 125
Atieh Monemi Bidgoli, Hassan Haghighi and Hamideh Sabouri
Purpose-based Policy Enforcement in Actor-based Systems . 140
Shahrzad Riahi, Ramtin Khosravi and Fatemeh Ghassemi
Quality-Aware Reactive Programming for the Internet of
Things . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .156
Jos´e Proen¸ca and Carlos Baquero
Implementing Open Call-by-Value . . . . . . . . . . . . . . . . . . . . . . 171
Beniamino Accattoli and Giulio Guerrieri
Gray-Box Conformance Testing for Symbolic Reactive State Machines . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 189
Masoumeh Taromirad and Mohammadreza Mousavi
LittleDarwin: a Feature-Rich and Extensible Mutation Testing
Framework for Large and Complex Java Systems. . . . . . . . . . 204
Ali Parsai, Alessandro Murgia and Serge Demeyer
Automatic Transition System Model Identifications for Network
Applications from Packet Traces . . . . . . . . . . . . . . . . . . . . . . . 219
Zeynab Sabahi Kaviani, Fatemeh Ghassemi and Fateme Bajelan
Flexible Transactional Coordination in the Peer Model . . . . . . 235
Eva K¨uhn
Performance Test Requirements Extraction Using Formal Specifications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 250
Zahra Rahimi Nassab, Hamideh Sabouri, Mohamad Jafari Monfared and Hassan Haghighi
A Privacy-Preserving Synchronization Protocol in Actor Models . . . . . . . . 254
Mahboubeh Samadi, Fatemeh Ghassemi and Ramtin Khosrav