Last update:
Wed Feb 7 10:50:58 MST 2024
W. Rance Cleaveland and
Tiziana Margaria and
Bernhard Steffen Editorial . . . . . . . . . . . . . . . 1--5
Pierre Wolper The meaning of ``formal'': from weak to
strong formal methods . . . . . . . . . 6--8
Bernhard Steffen and
Tiziana Margaria and
Volker Braun The Electronic Tool Integration
platform: concepts and design . . . . . 9--30
Volker Braun and
Tiziana Margaria and
Carsten Weise Integrating tools in the ETI platform 31--48
Tiziana Margaria and
Volker Braun and
Jürgen Kreileder Interacting with ETI: a user session . . 49--63
Kim G. Larsen and
B. Steffen and
C. Weise Continuous modeling of real-time and
hybrid systems: from concepts to tools 64--85
Rajeev Alur and
Thomas A. Real-time system = discrete system +
clock variables . . . . . . . . . . . . 86--109
Thomas A. Henzinger and
Pei-Hsin Ho and
Howard Wong-Toi HYTECH: a model checker for hybrid
systems . . . . . . . . . . . . . . . . 110--122
Sergio Yovine KRONOS: a verification tool for
real-time systems . . . . . . . . . . . 123--133
Kim G. Larsen and
Paul Pettersson and
Wang Yi Uppaal in a nutshell . . . . . . . . . . 134--152
Philippe Leblanc OMT and SDL based techniques and tools
for design, simulation and test
production of distributed systems . . . 153--165
Marius Bozga and
Jean-Claude Fernandez and
Alain Kerbrat and
Laurent Mounier Protocol verification with the ALDÉBARAN
toolset . . . . . . . . . . . . . . . . 166--183
Gregor Snelting Paul Feyerabend and software technology 1--5
Chris Hankin Program analysis tools . . . . . . . . . 6--12
Torben Amtoft and
Hanne Riis Nielson and
Flemming Nielson Behavior analysis for validating
communication patterns . . . . . . . . . 13--28
Michael Codish and
Bart Demoen and
Konstantinos Sagonas Semantics-based program analysis for
logic-based languages using XSB . . . . 29--45
Florian Martin PAG --- an efficient program analyzer
generator . . . . . . . . . . . . . . . 46--67
Mihaela Sighireanu and
Radu Mateescu Verification of the Link layer protocol
of the IEEE-1394 serial bus (FireWire):
an experiment with E-LOTOS . . . . . . . 68--88
Perdita Stevens A verification tool developer's vade
mecum . . . . . . . . . . . . . . . . . 89--94
Kurt Jensen Preface by the Section Editor: Kurt
Jensen . . . . . . . . . . . . . . . . . 95--97
Lars M. Kristensen and
Soren Christensen and
Kurt Jensen The practitioner's guide to coloured
Petri nets . . . . . . . . . . . . . . . 98--132
Jianli Xu and
Juha Kuusela Analyzing the execution architecture of
mobile phone software with colored Petri
nets . . . . . . . . . . . . . . . . . . 133--143
Steven Gordon and
Jonathan Billington Analysing a missile simulator with
coloured Petri nets . . . . . . . . . . 144--159
Gilles Moncelet and
Sòren Christensen and
Hamid Demmou and
Mario Paludetto and
José Porras Analysing a mechatronic system with
coloured Petri nets . . . . . . . . . . 160--167
Lee W. Wagenhals and
Insub Shin and
Alexander H. Levis Creating executable models of influence
nets with colored Petri nets . . . . . . 168--181
F. P. Burns and
A. M. Koelmans and
A. V. Yakovlev Analysing superscalar processor
architectures with coloured Petri nets 182--191
A. Pnueli and
O. Shtrichman and
M. Siegel The Code Validation Tool (CVT):
Automatic verification of a compilation
process . . . . . . . . . . . . . . . . 192--201
Thomas Friese and
Tiziana Margaria and
Alfred Hofmann Integrating printed and online
information . . . . . . . . . . . . . . 202--202
Steven D. Johnson A workshop on formal methods education:
held at Melbourne Florida in March 1998
[5]: an aggregation of opinions . . . . 203--207
Rance Cleaveland Pragmatics of model checking: an STTT
special section . . . . . . . . . . . . 208--218
Xiaoqun Du and
Scott A. Smolka and
Rance Cleaveland Local model checking and protocol
analysis . . . . . . . . . . . . . . . . 219--241
Henrik Reif Andersen and
Jorn Lind-Nielsen Partial model checking of modal
equations: a survey . . . . . . . . . . 242--259
Sérgio Vale Aguiar Campos and
Edmund Clarke Analysis and verification of real-time
systems using quantitative symbolic
algorithms . . . . . . . . . . . . . . . 260--269
Gerard J. Holzmann and
Anuj Puri A minimized automaton representation of
reachable states . . . . . . . . . . . . 270--278
E. M. Clarke and
O. Grumberg and
M. Minea and
D. Peled State space reduction using partial
order techniques . . . . . . . . . . . . 279--287
Carl Pixley and
Vigyan Singhal Model checking: a hardware design
perspective . . . . . . . . . . . . . . 288--306
C. Barry Jay Programming in FISh . . . . . . . . . . 307--315
George S. Avrunin and
James C. Corbett and
Matthew B. Dwyer Benchmarking finite-state verifiers . . 317--320
Gerard Holzmann and
Eli Najm and
Ahmed Serhrouchni SPIN model checking: an introduction . . 321--327
Yonit Kesten and
Amir Pnueli Control and data abstraction: the
cornerstones of practical formal
verification . . . . . . . . . . . . . . 328--342
Lynette I. Millett and
Tim Teitelbaum Issues in slicing PROMELA and its
applications to model checking, protocol
understanding, and simulation . . . . . 343--349
Willem Visser and
Howard Barringer Practical CTL$^*$ model checking: Should
SPIN be extended? . . . . . . . . . . . 350--365
Klaus Havelund and
Thomas Pressburger Model checking JAVA programs using JAVA
PathFinder . . . . . . . . . . . . . . . 366--381
René G. de Vries and
Jan Tretmans On-the-fly conformance testing using
SPIN . . . . . . . . . . . . . . . . . . 382--393
Moataz Kamel and
Stefan Leue Formalization and validation of the
General Inter-ORB Protocol (GIOP) using
PROMELA and SPIN . . . . . . . . . . . . 394--409
Alessandro Cimatti and
Edmund Clarke and
Fausto Giunchiglia and
Marco Roveri NUSMV: a new symbolic model checker . . 410--425
Fausto Giunchiglia and
Paolo Traverso Theorem proving in technology transfer:
the user's point of view . . . . . . . . 1--12
Matt Kaufmann Verification of Year 2000 conversion
rules using the ACL2 theorem prover . . 13--19
Ben L. Di Vito High-automation proofs for properties of
requirements models . . . . . . . . . . 20--31
Deepak Kapur and
Mahadevan Subramaniam Using an induction prover for verifying
arithmetic circuits . . . . . . . . . . 32--65
Serge Autexier and
Dieter Hutter and
Bruno Langenstein and
Heiko Mantel and
Georg Rock and
Axel Schairer and
Werner Stephan and
Roland Vogt and
Andreas Wolpers VSE: formal methods meet industrial
needs . . . . . . . . . . . . . . . . . 66--77
Paolo Traverso and
Piergiorgio Bertoli Mechanized result verification: an
industrial application . . . . . . . . . 78--92
Alexander Aiken and
Manuel Fähndrich and
Zhendong Su Detecting races in Relay Ladder Logic
programs . . . . . . . . . . . . . . . . 93--105
Ed Brinksma Verification is experimentation! . . . . 107--111
Rolf Drechsler and
Detlef Sieling Binary decision diagrams in theory and
practice . . . . . . . . . . . . . . . . 112--136
Randal E. Bryant and
Yirng-An Chen Verification of arithmetic circuits
using binary moment diagrams . . . . . . 137--155
Shin-ichi Minato Zero-suppressed BDDs and their
applications . . . . . . . . . . . . . . 156--170
Fabio Somenzi Efficient manipulation of decision
diagrams . . . . . . . . . . . . . . . . 171--181
Stefan Höreth A word-level graph manipulation package 182--192
Justin E. Harlow III and
Franc Brglez Design of experiments and evaluation of
BDD ordering heuristics . . . . . . . . 193--206
Janett Mohnke and
Paul Molitor and
Sharad Malik Application of BDDs in Boolean matching
techniques for formal logic
combinational verification . . . . . . . 207--216
Berna L. Massingill and
Timothy G. Mattson and
Beverly A. Sanders Parallel programming with a pattern
language $^*$ . . . . . . . . . . . . . 217--234
Alberto Bartoli and
Gianluca Dini and
Lanfranco Lopriore Application-controlled memory management
in a single address space environment 235--245
Rance Cleaveland Preface by the section editor . . . . . 247--249
Giorgio Delzanno and
Andreas Podelski Constraint-based deductive model
checking . . . . . . . . . . . . . . . . 250--270
Daniel Hirschkoff Bisimulation verification using the up
to techniques . . . . . . . . . . . . . 271--285
Christoph Kern and
Tarik Ono-Tesfaye and
Mark R. Greenstreet A light-weight framework for hardware
verification . . . . . . . . . . . . . . 286--313
Hubert Garavel and
César Viho and
Massimo Zendri System design of a CC-NUMA
multiprocessor architecture using formal
specification, model-checking,
co-simulation, and test generation . . . 314--331
Marieke Huisman and
Bart Jacobs and
Joachim van den Berg A case study in class library
verification: Java's vector class . . . 332--352
Magnus Lindahl and
Paul Pettersson and
Wang Yi Formal design and analysis of a gear
controller . . . . . . . . . . . . . . . 353--368
Kurt Jensen Preface by the section editor . . . . . 369--371
Gérard Berthelot and
Laure Petrucci Specification and validation of a
concurrent system: an educational
project . . . . . . . . . . . . . . . . 372--381
Leo Ojala and
Nisse Husberg and
Teemu Tynjälä Modelling and analysing a distributed
dynamic channel allocation algorithm for
mobile computing using high-level net
methods . . . . . . . . . . . . . . . . 382--393
Hartmann Genrich and
Robert Küffner and
Klaus Voss Executable Petri net models for the
analysis of metabolic pathways . . . . . 394--404
Bo Lindstrom Web-based interfaces for simulation of
coloured Petri net models . . . . . . . 405--416
S. Bernardi and
S. Donatelli and
A. Horváth Implementing compositionality for
stochastic Petri nets . . . . . . . . . 417--430
Matthias Anlauff and
Samarjit Chakraborty and
Philipp W. Kutter and
Alfonso Pierantonio and
Lothar Thiele Generating an action notation
environment from Montages descriptions 431--455
Alex Aizman Easy concurrency . . . . . . . . . . . . 456--468
David P. L. Simons and
Mariëlle I. A. Stoelinga Mechanical verification of the IEEE
1394a root contention protocol using
Uppaal2k . . . . . . . . . . . . . . . . 469--485
Ekkart Kindler and
Michael Weber The Petri Net Kernel: an infrastructure
for building Petri net tools . . . . . . 486--497
Mary Shaw What makes good research in software
engineering? . . . . . . . . . . . . . . 1--7
Klaus Havelund and
Willem Visser Program model checking as a new trend 8--20
Ed Brinksma and
Angelika Mader and
Ansgar Fehnker Verification and optimization of a PLC
control schedule . . . . . . . . . . . . 21--33
James C. Corbett and
Matthew B. Dwyer and
John Hatcliff and
Robby Expressing checkable properties of
dynamic systems: the Bandera
Specification Language . . . . . . . . . 34--56
Heikki Tauriainen and
Keijo Heljanko Testing LTL formula translation into
Büchi automata . . . . . . . . . . . . . 57--70
Scott D. Stoller Model-checking multi-threaded
distributed Java programs . . . . . . . 71--91
Dragan Bo\vsna\vcki and
Dennis Dams and
Leszek Holenderski Symmetric Spin . . . . . . . . . . . . . 92--106
Cindy Eisner Using symbolic CTL model checking to
verify the railway stations of
Hoorn-Kersenboogerd and Heerhugowaard 107--124
E. M. Clarke and
M. Fujita and
S. P. Rajan and
T. Reps and
S. Shankar and
T. Teitelbaum Program slicing for VHDL . . . . . . . . 125--137
Susanne Graf Preface by the section editor . . . . . 139--141
Marius Bozga and
Jean-Claude Fernandez and
Lucian Ghirvu Using static analysis to improve
automatic test generation . . . . . . . 142--152
Holger Hermanns and
Joost-Pieter Katoen and
Joachim Meyer-Kayser and
Markus Siegle A tool for model-checking Markov chains 153--172
Edmund Clarke and
Somesh Jha and
Will Marrero Efficient verification of security
protocols using partial-order reductions 173--188
Louise A. Dennis and
Graham Collins and
Michael Norrish and
Richard J. Boulton and
Konrad Slind and
Thomas F. Melham The PROSPER toolkit . . . . . . . . . . 189--210
Steven D. Johnson and
Yanhong A. Liu and
Yuchen Zhang A systematic incrementalization
technique and its application to
hardware design . . . . . . . . . . . . 211--223
Orna Kupferman and
Moshe Y. Vardi Vacuity detection in temporal model
checking . . . . . . . . . . . . . . . . 224--233
Hong Peng and
Sofi\`ene Tahar and
Ferhat Khendek Comparison of SPIN and VIS for protocol
verification . . . . . . . . . . . . . . 234--245
Theo C. Ruys and
Ed Brinksma Managing the verification trajectory . . 246--259
Jeannette M. Wing Platitudes and attitudes . . . . . . . . 261--265
Tiziana Margaria Preface by the section editor . . . . . 266--270
Alan Mycroft and
Richard Sharp Higher-level techniques for hardware
description and synthesis . . . . . . . 271--297
Mark D. Aagaard and
Byron Cook and
Nancy A. Day and
Robert B. Jones A framework for superscalar
microprocessor correctness statements 298--312
Skander Kort and
Sofi\`ene Tahar and
Paul Curzon Hierarchical formal verification using a
hybrid tool . . . . . . . . . . . . . . 313--322
Roope Kaivola and
Katherine Kohatsu Proof engineering in the large: formal
verification of Pentium\reg4
floating-point divider . . . . . . . . . 323--334
Fady Copty and
Amitai Irron and
Osnat Weissberg and
Nathan Kropp and
Gila Kamhi Efficient debugging in a formal
verification environment . . . . . . . . 335--348
Koen Claessen and
Mary Sheeran and
Satnam Singh Using Lava to design and verify
recursive and periodic sorters . . . . . 349--358
Xiaohua Kong and
Radu Negulescu and
Larry Weidong Ying Refinement-based formal verification
with heterogeneous timing . . . . . . . 359--370
César Muñoz and
Víctor Carreño and
Gilles Dowek and
Ricky Butler Formal verification of conflict
detection algorithms . . . . . . . . . . 371--380
Karim El Guemhioui A framework for distributing
object-oriented designs . . . . . . . . 381--396
Dieter Hogrefe Main issues in protocol testing . . . . 397--400
Bengt Jonsson and
Konstantinos Sagonas Preface by the section editors . . . . . 401--404
Lars-Åke Fredlund and
Dilian Gurov and
Thomas Noll and
Mads Dam and
Thomas Arts and
Gennady Chugunov A verification tool for ERLANG . . . . . 405--420
Erik Johansson and
Mikael Pettersson and
Konstantinos Sagonas and
Thomas Lindgren The development of the HiPE system:
design and experience report . . . . . . 421--436
Jakob Engblom and
Andreas Ermedahl and
Mikael Sjödin and
Jan Gustafsson and
Hans Hansson Worst-case execution-time analysis for
embedded real-time systems . . . . . . . 437--455
John Håkansson and
Bengt Jonsson and
Ola Lundqvist Generating online test oracles from
temporal logic specifications . . . . . 456--471
Mourad Debbabi and
Nancy Durgin and
Mohamed Mejri and
John C. Mitchell Security by typing . . . . . . . . . . . 472--495
Shoham Ben-David and
Orna Grumberg and
Tamir Heyman and
Assaf Schuster Scalable distributed on-the-fly symbolic
model checking . . . . . . . . . . . . . 496--504
Yifei Dong and
Xiaoqun Du and
Gerard J. Holzmann and
Scott A. Smolka Fighting livelock in the GNU i-protocol:
a case study in explicit-state model
checking . . . . . . . . . . . . . . . . 505--528
Tiziana Margaria and
Wang Yi Introductory paper: scalability aspects
of validation . . . . . . . . . . . . . 1--3
Poul F. Williams and
Henrik R. Andersen and
Henrik Hulgaard Satisfiability checking using Boolean
Expression Diagrams . . . . . . . . . . 4--14
Tuba Yavuz-Kahveci and
Tevfik Bultan A symbolic manipulator for automated
verification of reactive systems with
heterogeneous data types . . . . . . . . 15--33
Corina S. P\uas\uareanu and
Matthew B. Dwyer and
Willem Visser Finding feasible abstract
counter-examples . . . . . . . . . . . . 34--48
Thomas Ball and
Andreas Podelski and
Sriram K. Rajamani Boolean and Cartesian abstraction for
model checking C programs . . . . . . . 49--58
Brian Nielsen and
Arne Skou Automated test generation from timed
automata . . . . . . . . . . . . . . . . 59--77
Elsa L. Gunter and
Anca Muscholl and
Doron Peled Compositional message sequence charts 78--89
P. Chevalley and
P. Thévenod-Fosse A mutation analysis tool for Java
programs . . . . . . . . . . . . . . . . 90--103
Jaco van de Pol Introductory paper . . . . . . . . . . . 105--106
Tiziana Margaria and
Bernhard Steffen Lightweight coarse-grained coordination:
a scalable system-level approach . . . . 107--123
David Lugato and
Céline Bigot and
Yannick Valot and
Jean-Pierre Gallois and
Sébastien Gérard and
François Terrier Validation and automatic test generation
on UML models: the AGATHA approach . . . 124--139
A. Pretschner and
O. Slotosch and
E. Aiglstorfer and
S. Kriebel Model-based testing for real: The
inhouse card case study . . . . . . . . 140--157
Gordon Pace and
Nicolas Halbwachs and
Pascal Raymond Counter-example generation in symbolic
abstract model-checking . . . . . . . . 158--164
María del Mar Gallardo and
Jesús Martínez and
Pedro Merino and
Ernesto Pimentel aSPIN: a tool for abstract model
checking . . . . . . . . . . . . . . . . 165--184
Viktor Schuppan and
Armin Biere Efficient reduction of finite state
model checking to reachability analysis 185--204
Thomas Arts and
Clara Benac Earle and
John Derrick Development of a verified Erlang program
for resource locking . . . . . . . . . . 205--220
Conrado Daws and
Marta Kwiatkowska and
Gethin Norman Automatic verification of the IEEE 1394
root contention protocol with KRONOS and
PRISM . . . . . . . . . . . . . . . . . 221--236
Sylvie Boldo and
Marc Daumas Properties of two's complement floating
point notations . . . . . . . . . . . . 237--246
Stefan Edelkamp and
Stefan Leue and
Alberto Lluch-Lafuente Directed explicit-state model checking
in the validation of communication
protocols . . . . . . . . . . . . . . . 247--267
Giorgio Delzanno and
Jean-François Raskin and
Laurent Van Begin Covering sharing trees: a compact data
structure for parameterized verification 268--297
S. Purushothaman Iyer and
David Hislop and
Paul L. Jones and
Jaime Lee and
Frederick Pearce and
Stephen Van Albert Introductory paper . . . . . . . . . . . 299--300
John C. Martin Formal methods software engineering for
the CARA system . . . . . . . . . . . . 301--307
Rajeev Alur and
David Arney and
Elsa L. Gunter and
Insup Lee and
Jaime Lee and
Wonhong Nam and
Frederick Pearce and
Steve Van Albert and
Jiaxiang Zhou Formal specifications and analysis of
the computer-assisted resuscitation
algorithm (CARA) Infusion Pump Control
System . . . . . . . . . . . . . . . . . 308--319
Raoul Praful Jetley and
Cohan Carlos and
S. Purushothaman Iyer A case study on applying formal methods
to medical devices: computer-aided
resuscitation algorithm . . . . . . . . 320--330
Eugene W. Stark Formally specifying CARA in Java . . . . 331--350
Arnab Ray and
Rance Cleaveland Unit verification: the CARA experience 351--369
Luqi and
Z. Guan and
V. Berzins and
L. Zhang and
D. Floodeen and
V. Coskun and
J. Puett and
M. Brown Requirements-document-based prototyping
of CARA software . . . . . . . . . . . . 370--390
Lenore Zuck and
Paul Attie and
Agostino Cortesi Preface by the section editors . . . . . 1--3
Hardi Hungar and
Bernhard Steffen Behavior-based model construction . . . 4--14
Xavier Rival Certification of compiled assembly code
by invariant translation . . . . . . . . 15--37
Ping Yang and
C. R. Ramakrishnan and
Scott A. Smolka A logical encoding of the
$\pi$-calculus: model checking mobile
processes using tabled resolution . . . 38--66
Toh Ne Win and
Michael D. Ernst and
Stephen J. Garland and
Dilsun Kimathrlimath and
Nancy A. Lynch Using simulated execution in verifying
distributed algorithms . . . . . . . . . 67--76
Farn Wang Efficient verification of timed automata
with BDD-like data structures . . . . . 77--97
Joost-Pieter Katoen and
Perdita Stevens Guest editors' introduction:
Advancements and extensions of
verification techniques . . . . . . . . 99--101
HoonSang Jin and
Kavita Ravi and
Fabio Somenzi Fate and free will in error traces . . . 102--116
Patrice Godefroid and
Sarfraz Khurshid Exploring very large state spaces using
genetic algorithms . . . . . . . . . . . 117--127
Marta Kwiatkowska and
Gethin Norman and
David Parker Probabilistic symbolic model checking
with PRISM: a hybrid approach . . . . . 128--142
Fabrice Bouquet and
Bruno Legeard and
Fabien Peureux CLPS-B --- a constraint solver to
animate a B specification . . . . . . . 143--157
Klaus Havelund and
Grigore Ro\csu Efficient monitoring of safety
properties . . . . . . . . . . . . . . . 158--173
Sérgio Campos and
Orna Grumberg and
Karen Yorav and
Copty Fady Test sequence generation and model
checking using dynamic transition
relations . . . . . . . . . . . . . . . 174--182
Heiko Dörr and
Andy Schürr Introduction . . . . . . . . . . . . . . 183--185
G. Schopfer and
A. Yang and
L. von Wedel and
W. Marquardt CHEOPS: a tool-integration platform for
chemical process modelling and
simulation . . . . . . . . . . . . . . . 186--202
Sven Burmester and
Holger Giese and
Jörg Niere and
Matthias Tichy and
Jörg P. Wadsack and
Robert Wagner and
Lothar Wendehals and
Albert Zündorf Tool integration at the meta-model
level: the Fujaba approach . . . . . . . 203--218
Klaus Marius Hansen Thoth: a publish/subscribe architecture
for peer-to-peer tool integration . . . 219--230
Flavio Corradini and
Leonardo Mariani and
Emanuela Merelli An agent-based approach to tool
integration . . . . . . . . . . . . . . 231--244
Jean-Louis Colaço and
Marc Pouzet Type-based initialization analysis of a
synchronous dataflow language . . . . . 245--255
Matthew Dwyer and
Stefan Leue Special section on the algorithmics of
software model checking: Introductory
paper . . . . . . . . . . . . . . . . . 257--259
Alex Groce and
Willem Visser Heuristics for model checking Java
programs . . . . . . . . . . . . . . . . 260--276
Stefan Edelkamp and
Stefan Leue and
Alberto Lluch-Lafuente Partial-order reduction and trail
improvement in directed model checking 277--301
Radu Iosif Symmetry reductions for model checking
of concurrent dynamic software . . . . . 302--319
Giuseppe Della Penna and
Benedetto Intrigila and
Igor Melatti and
Enrico Tronci and
Marisa Venturini Zilli Exploiting transition locality in
automatic verification of finite-state
concurrent systems . . . . . . . . . . . 320--341
Lubo\vs Brim and
Orna Grumberg Special section on parallel and
distributed model checking: Introductory
paper . . . . . . . . . . . . . . . . . 1--3
Víctor Braberman and
Alfredo Olivero and
Fernando Schapachnik Issues in distributed timed model
checking: Building Zeus . . . . . . . . 4--18
Gerd Behrmann Distributed reachability analysis in
timed automata . . . . . . . . . . . . . 19--30
Michael D. Jones and
Jacob Sorber Parallel search for LTL violations . . . 31--42
Alexander Bell and
Boudewijn R. Haverkort Sequential and distributed model
checking of Petri nets . . . . . . . . . 43--60
Lubo\vs Brim and
Karen Yorav and
Jitka \vZídková Assumption-based distribution of CTL
model checking . . . . . . . . . . . . . 61--73
Stefan Blom and
Simona Orzan A distributed algorithm for strong
bisimulation reduction of state spaces 74--86
Armin Biere and
Ofer Strichman Introductory paper: Highlights from the
BMC'03 workshop and more . . . . . . . . 87--88
Toni Jussila and
Keijo Heljanko and
Ilkka Niemelä BMC via on-the-fly determinization . . . 89--101
Gianpiero Cabodi and
Alex Kondratyev and
Luciano Lavagno and
Sergio Nocco and
Stefano Quer and
Yosinori Watanabe A BMC-based formulation for the
scheduling problem of hardware systems 102--117
Rajeev Alur and
P. Madhusudan and
Wonhong Nam Symbolic computational techniques for
solving games . . . . . . . . . . . . . 118--128
Gianpiero Cabodi and
Sergio Nocco and
Stefano Quer Are BDDs still alive within sequential
verification? . . . . . . . . . . . . . 129--142
Bing Li and
Chao Wang and
Fabio Somenzi Abstraction refinement in symbolic model
checking using satisfiability as the
only decision procedure . . . . . . . . 143--155
Mukul R. Prasad and
Armin Biere and
Aarti Gupta A survey of recent advances in SAT-based
formal verification . . . . . . . . . . 156--173
Edmund Clarke and
Daniel Kroening and
Joël Ouaknine and
Ofer Strichman Computational challenges in bounded
model checking . . . . . . . . . . . . . 174--183
Martin Leucker and
Thomas Noll and
Perdita Stevens and
Michael Weber Functional programming languages for
verification tools: a comparison of
Standard ML and Haskell . . . . . . . . 184--194
Thomas Arts and
Jaco van de Pol Special section on formal methods for
industrial critical systems:
Introductory paper . . . . . . . . . . . 195--196
Richard Bubel and
Reiner Hähnle Integration of informal and formal
development of object-oriented
safety-critical software . . . . . . . . 197--211
Lilian Burdy and
Yoonsik Cheon and
David R. Cok and
Michael D. Ernst and
Joseph R. Kiniry and
Gary T. Leavens and
K. Rustan M. Leino and
Erik Poll An overview of JML tools and
applications . . . . . . . . . . . . . . 212--232
Achim D. Brucker and
Burkhart Wolff A verification approach to applied
system security . . . . . . . . . . . . 233--247
Andrew Butterfield and
Jim Woodcock prialt in Handel-C: an operational
semantics . . . . . . . . . . . . . . . 248--267
Jerker Hammarberg and
Simin Nadjm-Tehrani Formal verification of fault tolerance
in safety-critical reconfigurable
modules . . . . . . . . . . . . . . . . 268--279
Stefan Blom and
Simona Orzan Distributed state space minimization . . 280--291
Tiziana Margaria Introductory paper . . . . . . . . . . . 293--296
Claude Jard and
Thierry Jéron TGV: theory, principles and algorithms 297--315
César Viho Test distribution: a solution for
complex network system testing . . . . . 316--325
Andrea Baldini and
Alfredo Benso and
Paolo Prinetto System-level functional testing from UML
specifications in end-of-production
industrial environments . . . . . . . . 326--340
Annette Bunker and
Ganesh Gopalakrishnan and
Konrad Slind Live sequence charts applied to hardware
requirements specification and
verification . . . . . . . . . . . . . . 341--350
Ina Schieferdecker and
George Din and
Dimitrios Apostolidis Distributed functional and load tests
for Web services . . . . . . . . . . . . 351--360
Kenneth J. Turner Test generation for radiotherapy
accelerators . . . . . . . . . . . . . . 361--375
Bartholomäus Kellerer and
Manfred Reitenspiess Practical quality assurance for
standards-based, high-availability
middleware . . . . . . . . . . . . . . . 376--387
Hubert Garavel and
John Hatcliff Why you should definitely read this
special section . . . . . . . . . . . . 1--3
Gianfranco Ciardo and
Robert Marmorstein and
Radu Siminiceanu The saturation algorithm for symbolic
state-space exploration . . . . . . . . 4--25
Constantinos Bartzis and
Tevfik Bultan Efficient BDDs for bounded arithmetic
constraints . . . . . . . . . . . . . . 26--36
Radu Mateescu CAESAR\_SOLVE: a generic library for
on-the-fly resolution of
alternation-free Boolean equation
systems . . . . . . . . . . . . . . . . 37--56
L. Bozga and
Y. Lakhnech and
M. Périn Pattern-based abstraction for verifying
secrecy in protocols . . . . . . . . . . 57--76
Jan Friso Groote and
Frank van Ham Interactive visualization of large state
spaces . . . . . . . . . . . . . . . . . 77--91
Susanne Graf and
Òystein Haugen and
Ileana Ober and
Bran Selic Preface of ``Specification and
Validation of Real Time and Embedded
systems in UML'' . . . . . . . . . . . . 93--96
Jozef Hooman and
Mark B. van der Zwaag A semantics of communicating reactive
objects with timing . . . . . . . . . . 97--112
Susanne Graf and
Ileana Ober and
Iulian Ober A real-time profile for UML . . . . . . 113--127
Iulian Ober and
Susanne Graf and
Ileana Ober Validating timed UML models by
simulation and verification . . . . . . 128--145
Robert de Simone and
Charles André Towards a ``Synchronous Reactive'' UML
profile? . . . . . . . . . . . . . . . . 146--155
Juliana Küster-Filipe and
Stuart Anderson On a time enriched OCL liveness template 156--166
Kirsten Berkenkötter and
Stefan Bisanz and
Ulrich Hannemann and
Jan Peleska The HybridUML profile for UML 2.0 . . . 167--176
Kurt Jensen and
Andreas Podelski Tools and algorithms for the
construction and analysis of systems . . 177--179
Antti Valmari What the small Rubik's cube taught me
about data structures, information
theory, and randomisation . . . . . . . 180--194
Karsten Schmidt Automated generation of a progress
measure for the sweep-line method . . . 195--203
Gerd Behrmann and
Patricia Bouyer and
Kim G. Larsen and
Radek Pelánek Lower and upper bounds in zone-based
abstractions of timed automata . . . . . 204--215
Håkan L. S. Younes and
Marta Kwiatkowska and
Gethin Norman and
David Parker Numerical vs. statistical probabilistic
model checking . . . . . . . . . . . . . 216--228
Alex Groce and
Sagar Chaki and
Daniel Kroening and
Ofer Strichman Error explanation with distance metrics 229--247
Koushik Sen and
Grigore Rosu and
Gul Agha Online efficient predictive safety
analysis of multithreaded programs . . . 248--260
Yi Fang and
Nir Piterman and
Amir Pnueli and
Lenore Zuck Liveness with invisible ranking . . . . 261--279
Robby and
Edwin Rodríguez and
Matthew B. Dwyer and
John Hatcliff Checking JML specifications using an
extensible software model checking
framework . . . . . . . . . . . . . . . 280--299
John S. Fitzgerald and
Stefania Gnesi and
Dino Mandrioli The industrialization of formal methods 301--302
Steven P. Miller and
Alan C. Tribble and
Michael W. Whalen and
Mats P. E. Heimdahl Proving the shalls . . . . . . . . . . . 303--319
C. J. Fidge Formal change impact analyses for
emulated control software . . . . . . . 321--335
Alan Wassyng and
Mark Lawford Software tools for safety-critical
software development . . . . . . . . . . 337--354
Enrico Tronci Introductory Paper . . . . . . . . . . . 355--358
J. Strother Moore Inductive assertions and operational
semantics . . . . . . . . . . . . . . . 359--371
Hana Chockler and
Orna Kupferman and
Moshe Vardi Coverage metrics for formal verification 373--386
Malay K. Ganai and
Aarti Gupta and
Zijiang Yang and
Pranav Ashar Efficient distributed SAT and SAT-based
distributed Bounded Model Checking . . . 387--396
Giuseppe Della Penna and
Benedetto Intrigila and
Igor Melatti and
Enrico Tronci and
Marisa Venturini Zilli Finite horizon analysis of Markov Chains
with the Mur$\phi$ verifier . . . . . . 397--409
Sven Beyer and
Christian Jacobi and
Daniel Kröning and
Dirk Leinenbach and
Wolfgang J. Paul Putting it all together --- Formal
verification of the VAMP . . . . . . . . 411--430
Tiziana Margaria and
Bernhard Steffen Special Section on ``Leveraging Formal
Methods'' . . . . . . . . . . . . . . . 467--469
François Carcenac and
Frederic Boniol A formal framework for verifying
distributed embedded systems based on
abstraction methods . . . . . . . . . . 471--484
Jesper Andersen and
Ebbe Elsborg and
Fritz Henglein and
Jakob Grue Simonsen and
Christian Stefansen Compositional specification of
commercial contracts . . . . . . . . . . 485--516
Erwan Jahier and
Pascal Raymond and
Philippe Baufreton Case studies with Lurette V2 . . . . . . 517--530
Jens Bæk Jòrgensen and
Sòren Christensen and
Antti-Pekka Tuovinen and
Jianli Xu Tool Support for Estimating the Memory
Usage of Mobile Phone Software . . . . . 531--545
Yamine Ait-Ameur and
Mickael Baron Formal and experimental validation
approaches in HCI systems design based
on a shared event B model . . . . . . . 547--563
M. Alpuente and
D. Ballis and
M. Falaschi Rule-based verification of Web sites . . 565--585
Christopher A. Rouff and
Michael G. Hinchey and
Walter F. Truszkowski and
James L. Rash Experiences applying formal approaches
in the development of swarm-based space
exploration systems . . . . . . . . . . 587--603
Peter Buchholz and
Joost-Pieter Katoen and
Marcel Verhoef Guest Editors' introduction:
quantitative analysis of real-time
embedded systems . . . . . . . . . . . . 605--606
Joern Ploennigs and
Mario Neugebauer and
Klaus Kabitzsch Automated model generation for
performance engineering of building
automation networks . . . . . . . . . . 607--620
Deepak D'Souza and
Pavithra Prabhakar On the expressiveness of MTL in the
pointwise and continuous semantics . . . 1--4
Marco Bozzano and
Adolfo Villafiorita The FSAP/NuSMV-SA Safety Analysis
Platform . . . . . . . . . . . . . . . . 5--24
Michael Huth Some current topics in model checking 25--36
Aleksandar Dimovski and
Ranko Lazi\'c Compositional software verification
based on game semantics and process
algebra . . . . . . . . . . . . . . . . 37--51
Dimitar P. Guelev and
Mark D. Ryan and
Pierre Yves Schobbens Model-checking the preservation of
temporal properties upon feature
integration . . . . . . . . . . . . . . 53--62
Radu I. Siminiceanu and
Gianfranco Ciardo Formal verification of the NASA runway
safety monitor . . . . . . . . . . . . . 63--76
Cécile Braunstein and
Emmanuelle Encrenaz CTL-property Transformations along an
Incremental Design Process . . . . . . . 77--88
Shobha Vasudevan and
E. Allen Emerson and
Jacob A. Abraham Improved verification of hardware
designs through antecedent conditioned
slicing . . . . . . . . . . . . . . . . 89--101
Dragan Ga\vsevi\'c and
Dragan Djuri\'c and
Vladan Deved\vzi\'c MDA-based Automatic OWL Ontology
Development . . . . . . . . . . . . . . 103--117
Orna Grumberg and
Shmuel Katz VeriTech: a framework for translating
among model description notations . . . 119--132
Mauro Pezz\`e Introduction to the special section on
FASE 2003 . . . . . . . . . . . . . . . 133--134
Wim Vanderperren and
Davy Suvée and
Bruno De Fraine and
Viviane Jonckers Aspect-oriented Component Composition in
PacoSuite Through Invasive Composition
Adapters . . . . . . . . . . . . . . . . 135--154
Ioana Sora and
Pierre Verbaeten and
Yolande Berbers CCDL: the Composable Components
Description Language . . . . . . . . . . 155--168
Claus Pahl An ontology for software component
matching . . . . . . . . . . . . . . . . 169--178
Vieri del Bianco and
Luigi Lavazza and
Marco Mauri and
Giuseppe Occorso Towards UML-based formal specifications
of component-based real-time software 179--192
Reiko Heckel and
Marc Lohmann Model-driven development of reactive
information systems: from graph
transformation rules to JML contracts 193--207
Kurt Jensen Special section on coloured Petri nets 209--212
Kurt Jensen and
Lars Michael Kristensen and
Lisa Wells Coloured Petri Nets and CPN Tools for
modelling and validation of concurrent
systems . . . . . . . . . . . . . . . . 213--254
Brice Mitchell and
Lars Michael Kristensen and
Lin Zhang Formal specification and state space
analysis of an operational planning
process . . . . . . . . . . . . . . . . 255--267
Jonathan Billington and
Bing Han Modelling and analysing the functional
behaviour of TCP's connection management
procedures . . . . . . . . . . . . . . . 269--304
Lin Liu and
Jonathan Billington Verification of the Capability Exchange
Signalling protocol . . . . . . . . . . 305--326
Maja Pesic and
Wil M. P. van der Aalst Modelling work distribution mechanisms
using Colored Petri Nets . . . . . . . . 327--352
Ricardo J. Machado and
Kristian Bisgaard Lassen and
Sérgio Oliveira and
Marco Couto and
Patrícia Pinto Requirements Validation: Execution of
UML Models with CPN Tools . . . . . . . 353--369
Guy Edward Gallasch and
Jonathan Billington and
Somsak Vanit-Anunchai and
Lars Michael Kristensen Checking safety properties on-the-fly
with the sweep-line method . . . . . . . 371--391
C. Lakos and
L. Petrucci Modular state space exploration for
timed Petri nets . . . . . . . . . . . . 393--411
Roberto Bagnara and
Patricia M. Hill and
Enea Zaffanella Widening operators for powerset domains 413--414
Michel Wermelinger and
Tiziana Margaria and
Maura Cerioli Introduction to the special section on
fundamental approaches to software
engineering . . . . . . . . . . . . . . 415--416
Georg Jung and
John Hatcliff A correlation framework for the CORBA
component model . . . . . . . . . . . . 417--427
Marsha Chechik and
Arie Gurfinkel A framework for counterexample
generation and exploration . . . . . . . 429--445
Grégoire Hamon and
John Rushby An operational semantics for Stateflow 447--456
Ruth Breu and
Gerhard Popp and
Muhammad Alam Model based development of access
policies . . . . . . . . . . . . . . . . 457--470
Kim G. Larsen and
Ulrik Nyman and
Andrzej Wasowski Modeling software product lines using
color-blind transition systems . . . . . 471--487
Venkatesh Prasad Ranganath and
John Hatcliff Slicing concurrent Java programs using
Indus and Kaveri . . . . . . . . . . . . 489--504
Dirk Beyer and
Thomas A. Henzinger and
Ranjit Jhala and
Rupak Majumdar The software model checker \sc Blast . . 505--525
Jan Jürjens and
Pasha Shabalin Tools for secure systems development
with UML . . . . . . . . . . . . . . . . 527--544
Kurt Jensen Special section on Coloured Petri Nets 1--3
Lars M. Kristensen and
Peter Mechlenborg and
Lin Zhang and
Brice Mitchell and
Guy E. Gallasch Model-based development of a course of
action scheduling tool . . . . . . . . . 5--14
Jens Bæk Jòrgensen and
Kristian Bisgaard Lassen and
Wil M. P. van der Aalst From task descriptions via colored Petri
nets towards an implementation of a new
electronic patient record workflow
system . . . . . . . . . . . . . . . . . 15--28
Somsak Vanit-Anunchai and
Jonathan Billington and
Guy Edward Gallasch Analysis of the Datagram Congestion
Control Protocol's connection management
procedures using the sweep-line method 29--56
A. Rozinat and
R. S. Mans and
M. Song and
W. M. P. van der Aalst Discovering colored Petri nets from
event logs . . . . . . . . . . . . . . . 57--74
Guy Edward Gallasch and
Nimrod Lilith and
Jonathan Billington and
Lin Zhang and
Axel Bender and
Benjamin Francis Modelling defence logistics networks . . 75--93
F. Gottschalk and
W. M. P. van der Aalst and
M. H. Jansen-Vullers and
H. M. W. Verbeek Protos2CPN: using colored Petri nets for
configuring and testing business
processes . . . . . . . . . . . . . . . 95--110
Holger Hermanns and
Jens Palsberg Improving the effectiveness of system
verification . . . . . . . . . . . . . . 111--112
Dina Thomas and
Supratik Chakraborty and
Paritosh Pandya Efficient guided symbolic reachability
using reachability expressions . . . . . 113--129
Alex Groce and
Rajeev Joshi Exploiting traces in static program
analysis: better model checking through
printfs . . . . . . . . . . . . . . . . 131--144
Atul Gupta and
Pankaj Jalote An approach for experimentally
evaluating effectiveness and efficiency
of coverage criteria for software
testing . . . . . . . . . . . . . . . . 145--160
Javier Esparza and
Pradeep Kanade and
Stefan Schwoon A negative result on depth-first net
unfoldings . . . . . . . . . . . . . . . 161--166
Rachid Hadjidj and
Hanifa Boucheneb Improving state class constructions for
CTL* model checking of time Petri nets 167--184
Michael Leuschel and
Michael Butler ProB: an automated analysis toolset for
the B method . . . . . . . . . . . . . . 185--203
Wilhelm Schäfer and
Matthias Tichy Introduction to the special section on
self-optimizing mechatronic systems . . 205--206
Sven Burmester and
Holger Giese and
Eckehard Münch and
Oliver Oberschelp and
Florian Klein and
Peter Scheideler Tool support for the design of
self-optimizing mechatronic multi-agent
systems . . . . . . . . . . . . . . . . 207--222
Katrin Witting and
Bernd Schulz and
Michael Dellnitz and
Joachim Böcker and
Norbert Fröhleke A new approach for online multiobjective
optimization of mechatronic systems . . 223--231
Benno Stein Coping with large design spaces: design
problem solving in fluidic engineering 233--245
Mircea Trofin and
John Murphy Static verification of component
composition in contextual composition
frameworks . . . . . . . . . . . . . . . 247--261
Goran Frehse PHAVer: algorithmic verification of
hybrid systems past HyTech . . . . . . . 263--279
Ina Schieferdecker and
Jens Grabowski Introduction to the special section on
advances in test automation: the
evolution of TTCN-3 . . . . . . . . . . 281--283
Martin Botteck and
Thomas Deiß Introduction of TTCN-3 into the product
development process: considerations from
an electronic devices developer point of
view . . . . . . . . . . . . . . . . . . 285--289
Andrej Pietschker Automating test automation . . . . . . . 291--295
Markus Warken From testing to anti-product development 297--307
Helmut Neukirchen and
Benjamin Zeiss and
Jens Grabowski An approach to quality engineering of
TTCN-3 test specifications . . . . . . . 309--326
Stephan Schulz Test suite development with TTCN-3
libraries . . . . . . . . . . . . . . . 327--336
Ariel Sabiguero and
Anthony Baire and
César Viho Automatic CoDec generation to reduce
test engineering cost . . . . . . . . . 337--346
Thomas Deiß Refactoring and converting a TTCN-2 test
suite . . . . . . . . . . . . . . . . . 347--352
Michael Gläser and
Sebastian Müller and
Axel Rennoch and
Peter Schmitting Standardized TTCN-3 specifications for
SIP-ISUP/ISDN interworking testing . . . 353--358
George Din An IMS Performance Benchmark
Implementation based on the TTCN-3
Language . . . . . . . . . . . . . . . . 359--370
Bernard Stepien and
Liam Peyton and
Pulei Xiong Framework testing of Web applications
using TTCN-3 . . . . . . . . . . . . . . 371--381
Ina Schieferdecker and
Juergen Grossmann Testing hybrid control systems with
TTCN-3: an overview on continuous TTCN-3 383--400
Sébastien Bardin and
Alain Finkel and
Jérôme Leroux and
Laure Petrucci FAST: acceleration from theory to
practice . . . . . . . . . . . . . . . . 401--424
Jörn Ossowski and
Christel Baier A uniform framework for weighted
decision diagrams and its implementation 425--441
Radek Pelánek Properties of state spaces and their
applications . . . . . . . . . . . . . . 443--454
Ali Ebnenasir and
Sandeep S. Kulkarni and
Anish Arora FTSyn: a framework for automatic
synthesis of fault-tolerance . . . . . . 455--471
Alessandro Marchetto Special section on testing and security
of Web systems . . . . . . . . . . . . . 473--476
Alessandro Marchetto and
Filippo Ricca and
Paolo Tonella A case study-based comparison of Web
testing techniques applied to AJAX Web
applications . . . . . . . . . . . . . . 477--492
Antonio Carzaniga and
Alessandra Gorla and
Mauro Pezz\`e Healing Web applications through
automatic workarounds . . . . . . . . . 493--502
Graham Hughes and
Tevfik Bultan Automated verification of access control
policies using a SAT solver . . . . . . 503--520
Sebastian Kinder and
Rolf Drechsler Modeling and proving functional
completeness in formal verification of
counting heads . . . . . . . . . . . . . 521--534
Antti Valmari Software model checking is a rich
research field . . . . . . . . . . . . . 1--11
I. Melatti and
R. Palmer and
G. Sawaya and
Y. Yang and
R. M. Kirby and
others Parallel and distributed model checking
in Eddy . . . . . . . . . . . . . . . . 13--25
Klaus Dräger and
Bernd Finkbeiner and
Andreas Podelski Directed model checking with
distance-preserving abstractions . . . . 27--37
Dragan Bosnacki and
Stefan Leue and
Alberto Lluch Lafuente Partial-order reduction for general
state exploring algorithms . . . . . . . 39--51
Saswat Anand and
Corina S. Pasareanu and
Willem Visser Symbolic execution with abstraction . . 53--67
Alessandro Armando and
Jacopo Mantovani and
Lorenzo Platania Bounded model checking of software using
SMT solvers instead of SAT solvers . . . 69--83
Michael Huth and
Orna Grumberg Special section on advances in
reachability analysis and decision
procedures: contributions to
abstraction-based system verification 85--94
Randal E. Bryant and
Daniel Kroening and
Joël Ouaknine and
Sanjit A. Seshia and
Ofer Strichman and
Bryan Brady An abstraction-based decision procedure
for bit-vector arithmetic . . . . . . . 95--104
Shaunak Chatterjee and
Shuvendu K. Lahiri and
Shaz Qadeer and
Zvonimir Rakamari\'c A low-level memory model and an
accompanying reachability predicate . . 105--116
Andy Jinqing Yu and
Gianfranco Ciardo and
Gerald Lüttgen Decision-diagram-based techniques for
bounded reachability checking of
asynchronous systems . . . . . . . . . . 117--131
Lili Tan The worst-case execution time tool
challenge 2006 . . . . . . . . . . . . . 133--152
Chryssis Georgiou and
Nancy Lynch and
Panayiotis Mavrommatis and
Joshua A. Tauber Automated implementation of complex
distributed algorithms specified in the
IOA language . . . . . . . . . . . . . . 153--171
Mike Hinchey and
Tiziana Margaria and
Bernhard Steffen Guest Editor's introduction . . . . . . 173--174
Boutheina Chetali and
Quang-Huy Nguyen An automated testing experiment for
layered embedded C code . . . . . . . . 175--185
Bastian Schlich and
Stefan Kowalewski Model checking C source code for
embedded systems . . . . . . . . . . . . 187--202
Eric Van Wyk and
Mats Per Erik Heimdahl Flexibility in modeling languages and
tools: a call to arms . . . . . . . . . 203--215
Dominique Cansell and
Dominique Méry and
Cyril Proch System-on-chip design by proof-based
refinement . . . . . . . . . . . . . . . 217--238
Yamine Ait-Ameur and
Mickael Baron and
Nadjet Kamel and
Jean-Marc Mota Encoding a process algebra using the
Event B method Application to the
validation of human-computer
interactions . . . . . . . . . . . . . . 239--253
David Déharbe and
Silvio Ranise Satisfiability solving for software
verification . . . . . . . . . . . . . . 255--260
Alexandra Desmoulin and
César Viho Formalizing interoperability for test
case generation purpose . . . . . . . . 261--267
Karen Yorav Haifa verification conference 2007 . . . 269--272
Benny Pasternak and
Shmuel Tyszberowicz and
Amiram Yehudai GenUTest: a unit test and mock aspect
generation tool . . . . . . . . . . . . 273--290
Shai Fine and
Laurent Fournier and
Avi Ziv Using Bayesian networks and virtual
coverage to hit hard-to-reach events . . 291--305
Harald Raffelt and
Maik Merten and
Bernhard Steffen and
Tiziana Margaria Dynamic testing via automata learning 307--324
Domagoj Babi\'c and
Alan J. Hu Approximating the safely reusable set of
learned facts . . . . . . . . . . . . . 325--338
Corina S. Pasareanu and
Willem Visser A survey of new trends in symbolic
execution for software testing and
analysis . . . . . . . . . . . . . . . . 339--353
Tiziana Margaria and
Mieke Massink Preface . . . . . . . . . . . . . . . . 355--357
Pedro de la Cámara and
María del Mar Gallardo and
Pedro Merino and
David Sanán Checking the reliability of socket based
communication software . . . . . . . . . 359--374
Anton J. Wijs and
Jaco C. van de Pol and
Elena M. Bortnik Solving scheduling problems by untimed
model checking: The clinical chemical
analyser case study . . . . . . . . . . 375--392
Harald Raffelt and
Bernhard Steffen and
Therese Berg and
Tiziana Margaria LearnLib: a framework for extrapolating
behavioral models . . . . . . . . . . . 393--407
Jan Mikác and
Paul Caspi Flush: an example of development by
refinements in SCADE/Lustre . . . . . . 409--418
Filippo Ricca and
Liu Chao Special section on Web Systems Evolution 419--425
Alessandro Marchetto and
Filippo Ricca From objects to services: toward a
stepwise migration approach for Java
applications . . . . . . . . . . . . . . 427--440
Harry M. Sneed A pilot project for migrating COBOL code
to Web services . . . . . . . . . . . . 441--451
Keisuke Nakano and
Zhenjiang Hu and
Masato Takeichi Consistent Web site updating based on
bidirectional transformation . . . . . . 453--468
Giuseppe Scanniello and
Damiano Distante and
Michele Risi An approach and an Eclipse-based
environment for enhancing the navigation
structure of Web sites . . . . . . . . . 469--484
Mario Luca Bernardi and
Giuseppe Antonio Di Lucca and
Damiano Distante The RE-UWA approach to recover user
centered conceptual models from Web
applications . . . . . . . . . . . . . . 485--501
Brian Chan and
King Chun Foo and
Lionel Marks and
Ying Zou An approach for estimating the time
needed to perform code changes in
business applications . . . . . . . . . 503--515
Yamine Ait Ameur and
Frédéric Boniol and
Virginie Wiels Toward a wider use of formal methods for
aerospace systems design and
verification . . . . . . . . . . . . . . 1--7
Daniel Plagge and
Michael Leuschel Seven at one stroke: LTL model checking
for high-level specifications in B, Z,
CSP, and more . . . . . . . . . . . . . 9--21
Andreas Bauer and
Martin Leucker and
Christian Schallhart and
Michael Tautschnig Don't care in SMT: building flexible yet
efficient abstraction/refinement solvers 23--37
Joris Rehm Proved development of the real-time
properties of the IEEE 1394 Root
Contention Protocol with the event-B
method . . . . . . . . . . . . . . . . . 39--51
Shlomi Dolev and
Ori Gersten A framework for robust active super tier
systems . . . . . . . . . . . . . . . . 53--67
Richard H. Carver and
Yu Lei A class library for implementing,
testing, and debugging concurrent
programs . . . . . . . . . . . . . . . . 69--88
Dragan Bosnacki and
Stefan Edelkamp Model checking software: on some new
waves and some evergreens . . . . . . . 89--95
Michael Weber An embeddable virtual machine for state
space generation . . . . . . . . . . . . 97--111
Yu Yang and
Xiaofang Chen and
Ganesh Gopalakrishnan and
Robert M. Kirby Distributed dynamic partial order
reduction . . . . . . . . . . . . . . . 113--122
Kristin Y. Rozier and
Moshe Y. Vardi LTL satisfiability checking . . . . . . 123--137
J. Barnat and
L. Brim and
P. Rockai Scalable shared memory LTL model
checking . . . . . . . . . . . . . . . . 139--153
Sami Evangelista and
Christophe Pajault Solving the ignoring problem for partial
order reduction . . . . . . . . . . . . 155--170
Arend Rensink and
Pieter Van Gorp Graph transformation tool contest 2008 171--181
Javier Pérez and
Yania Crespo and
Berthold Hoffmann and
Tom Mens A case study to evaluate the suitability
of graph transformation tools for
program refactoring . . . . . . . . . . 183--199
Olaf Muliawan and
Dirk Janssens Model refactoring using MoTMoT . . . . . 201--209
Ákos Horváth and
Gábor Bergmann and
István Ráth and
Dániel Varró Experimental assessment of combining
pattern matching strategies with VIATRA2 211--230
Tamás Mészáros and
Gergely Mezei and
Tihamér Levendovszky and
Márk Asztalos Manual and automated performance
optimization of model transformation
systems . . . . . . . . . . . . . . . . 231--243
Enrico Biermann and
Claudia Ermel and
Leen Lambers and
Ulrike Prange and
Olga Runge and
others Introduction to AGG and EMF Tiger by
modeling a Conference Scheduling System 245--261
Edgar Jakumeit and
Sebastian Buchwald and
Moritz Kroll GrGen.NET: The expressive, convenient
and fast graph rewrite system . . . . . 263--271
Naouel Moha and
Sagar Sen and
Cyril Faucher and
Olivier Barais and
Jean-Marc Jézéquel Evaluation of Kermeta for solving
graph-based problems . . . . . . . . . . 273--285
Leif Geiger and
Albert Zündorf Fujaba case studies for GraBaTs 2008:
lessons learned . . . . . . . . . . . . 287--304
Angelika Mader and
Henrik Bohnenkamp and
Yaroslav S. Usenko and
David N. Jansen and
Johann Hurink and
Holger Hermanns Synthesis and stochastic assessment of
cost-optimal schedules . . . . . . . . . 305--318
Jocelyn Simmonds and
Jessica Davies and
Arie Gurfinkel and
Marsha Chechik Exploiting resolution proofs to speed up
LTL vacuity detection for BMC . . . . . 319--335
Vincent Beaudenon and
Emmanuelle Encrenaz and
Sami Taktak Data decision diagrams for Promela
systems analysis . . . . . . . . . . . . 337--352
Holger Krahn and
Bernhard Rumpe and
Steven Völkel MontiCore: a framework for compositional
development of domain specific languages 353--372
Adam Bakewell and
Aleksandar Dimovski and
Dan R. Ghica and
Ranko Lazi\'c Data-abstraction refinement: a game
semantic approach . . . . . . . . . . . 373--389
Giacomo Bucci and
Laura Carnevali and
Lorenzo Ridi and
Enrico Vicario Oris: a tool for modeling, verification
and evaluation of real-time systems . . 391--403
Daniel Kroening and
Tiziana Margaria Verified software: theories, tools and
experiments . . . . . . . . . . . . . . 405--408
Arie Gurfinkel and
Sagar Chaki Combining predicate and numeric
abstraction for software model checking 409--427
Patrice Chalin and
Robby and
Perry R. James and
Jooyong Lee and
George Karabotsos Towards an industrial grade IVE for Java
and next generation research platform
for JML . . . . . . . . . . . . . . . . 429--446
Jean-Raymond Abrial and
Michael Butler and
Stefan Hallerstede and
Thai Son Hoang and
Farhad Mehta and
others Rodin: an open toolset for modelling and
reasoning in Event-B . . . . . . . . . . 447--466
David R. Cok Improved usability and performance of
SMT solvers for debugging specifications 467--481
Corina S. Pasareanu New results in software model checking
and analysis . . . . . . . . . . . . . . 1--2
Ernst Moritz Hahn and
Holger Hermanns and
Lijun Zhang Probabilistic reachability for
parametric Markov models . . . . . . . . 3--19
Dragan Bosnacki and
Stefan Edelkamp and
Damian Sulewski and
Anton Wijs Parallel probabilistic model checking on
general purpose graphics processors . . 21--35
Nicholas Kidd and
Peter Lammich and
Tayssir Touili and
Thomas Reps A decision procedure for detecting
atomicity violations for communicating
processes with locks . . . . . . . . . . 37--60
Junghee Lim and
Akash Lal and
Thomas Reps Symbolic analysis via semantic
reinterpretation . . . . . . . . . . . . 61--87
Sebastian Schmerl and
Michael Vogel and
Hartmut König Using model checking to identify errors
in intrusion detection signatures . . . 89--106
Ying Zou and
Ji Wu and
Kenny Wong Guest editors' introduction to the
special section from the International
Symposium on Web Systems Evolution . . . 107--109
Kinga Dobolyi and
Elizabeth Soechting and
Westley Weimer Automating regression testing using
Web-based application similarities . . . 111--129
Alessandro Marchetto and
Roberto Tiella and
Paolo Tonella and
Nadia Alshahwan and
Mark Harman Crawlability metrics for automated Web
testing . . . . . . . . . . . . . . . . 131--149
Marco Torchiano and
Filippo Ricca and
Alessandro Marchetto Are Web applications more defect-prone
than desktop applications? . . . . . . . 151--166
Adina Mosincat and
Walter Binder Automated maintenance of service
compositions with SLA violation
detection and dynamic binding . . . . . 167--179
Marco D'Ambros and
Michele Lanza and
Mircea Lungu and
Romain Robbes On porting software visualization tools
to the web . . . . . . . . . . . . . . . 181--200
Hana Chockler and
Alan J. Hu Preface . . . . . . . . . . . . . . . . 201--205
Yoram Adler and
Dale Blue and
Thomas Conti and
Richard Prewitt and
Shmuel Ur Evaluating workloads using comparative
functional coverage . . . . . . . . . . 207--221
Cyrille Artho Iterative delta debugging . . . . . . . 223--246
Dorit Baras and
Shai Fine and
Laurent Fournier and
Dan Geiger and
Avi Ziv Automatic boosting of cross-product
coverage using Bayesian networks . . . . 247--261
Omer Bar-Ilan and
Oded Fuhrmann and
Shlomo Hoory and
Ohad Shacham and
Ofer Strichman Reducing the size of resolution proofs
in linear time . . . . . . . . . . . . . 263--272
K. Bauer and
R. Gentilini and
K. Schneider A uniform approach to three-valued
semantics for $\mu$-calculus on
abstractions of hybrid automata . . . . 273--287
Harald Fecher and
Sharon Shoham Local abstraction-refinement for the
$\mu$-calculus . . . . . . . . . . . . . 289--306
Lei Bu and
Xuandong Li Path-oriented bounded reachability
analysis of composed linear hybrid
systems . . . . . . . . . . . . . . . . 307--317
Roberto Sebastiani and
Stefano Tonetta and
Moshe Y. Vardi Symbolic systems, explicit properties:
on hybrid approaches for LTL symbolic
model checking . . . . . . . . . . . . . 319--335
Liana Barachisio Lisboa and
Vinicius Cardoso Garcia and
Eduardo Santana de Almeida and
Silvio Romero de Lemos Meira ToolDAy: a tool for domain analysis . . 337--353
Qiang Guo and
John Derrick Formally based tool support for model
checking Erlang applications . . . . . . 355--376
Olga Brukman and
Shlomi Dolev Recovery oriented programming: runtime
monitoring of safety and liveness . . . 377--395
Jean-Christophe Filliâtre Deductive software verification . . . . 397--403
Pascal Cuoq and
Benjamin Monate and
Anne Pacalet and
Virgile Prevosto Functional dependencies of C functions
via weakest pre-conditions . . . . . . . 405--417
Tjark Weber SMT solvers: new oracles for the HOL
theorem prover . . . . . . . . . . . . . 419--429
Kalou Cabrera Castillos and
Frédéric Dadeau and
Jacques Julliand Scenario-based testing from UML/OCL
behavioral models: Application to POSIX
compliance . . . . . . . . . . . . . . . 431--448
Daisuke Ishii and
Kazunori Ueda and
Hiroshi Hosobe An interval-based SAT modulo ODE solver
for model checking nonlinear hybrid
systems . . . . . . . . . . . . . . . . 449--461
Leo Freitas and
John McDermott Formal methods for security in the Xenon
hypervisor . . . . . . . . . . . . . . . 463--489
Neil D. Jones and
Markus Müller-Olm Preface to a special section on
verification, model checking, and
abstract interpretation . . . . . . . . 491--493
Nicholas Kidd and
Thomas Reps and
Julian Dolby and
Mandana Vaziri Finding concurrency-related bugs using
random isolation . . . . . . . . . . . . 495--518
Ankur Taly and
Sumit Gulwani and
Ashish Tiwari Synthesizing switching logic using
constraint solving . . . . . . . . . . . 519--535
Kousha Etessami and
Patrice Godefroid An abort-aware model of transactional
programming . . . . . . . . . . . . . . 537--551
Michal Rutkowski and
Ranko Lazi\'c and
Marcin Jurdzi\'nski Average-price-per-reward games on hybrid
automata with strong resets . . . . . . 553--569
Patrice Godefroid and
Nir Piterman LTL generalized model checking revisited 571--584
Vincent Laviron and
Francesco Logozzo SubPolyhedra: a family of numerical
abstract domains for the (more) scalable
inference of linear inequalities . . . . 585--601
Natasha Sharygina and
Stefano Tonetta and
Aliaksei Tsitovich An abstraction refinement approach
combining precise and approximated
techniques . . . . . . . . . . . . . . . 1--14
Amir Hossein Ghamarian and
Maarten de Mol and
Arend Rensink and
Eduardo Zambon and
Maria Zimakova Modelling and analysis using GROOVE . . 15--40
Shmuel Katz and
David Faitelson The Common Aspect Proof Environment . . 41--52
Ananda Basu and
Saddek Bensalem and
Marius Bozga and
Beno\^\it Delahaye and
Axel Legay Statistical abstraction and
model-checking of large heterogeneous
systems . . . . . . . . . . . . . . . . 53--72
Alain Denise and
Marie-Claude Gaudel and
Sandrine-Dominique Gouraud and
Richard Lassaigne and
Johan Oudinet and
others Coverage-biased random exploration of
large models and application to testing 73--93
Georgia Penido Safe and
Claudionor Coelho and
Luiz Filipe M. Vieira and
Celina Gomes Do Val and
Jose Augusto Nacif and
others Selection of formal verification
heuristics for parallel execution . . . 95--108
Parosh Aziz Abdulla Regular model checking . . . . . . . . . 109--118
Axel Legay Extrapolating (omega-)regular model
checking . . . . . . . . . . . . . . . . 119--143
Ahmed Bouajjani and
Tayssir Touili Widening techniques for regular tree
model checking . . . . . . . . . . . . . 145--165
Ahmed Bouajjani and
Peter Habermehl and
Adam Rogalewicz and
Tomás Vojnar Abstract regular (tree) model checking 167--191
Bernard Boigelot Domain-specific regular acceleration . . 193--206
Giorgio Delzanno and
Ahmed Rezine A lightweight regular model checking
approach for parameterized systems . . . 207--222
Parosh Aziz Abdulla and
Bengt Jonsson and
Marcus Nilsson and
Julien d'Orso and
Mayank Saksena Regular model checking for LTL(MSO) . . 223--241
Oleg Sokolsky and
Klaus Havelund and
Insup Lee Introduction to the special section on
runtime verification . . . . . . . . . . 243--247
Patrick O'Neil Meredith and
Dongyun Jin and
Dennis Griffith and
Feng Chen and
Grigore Rosu An overview of the MOP runtime
verification framework . . . . . . . . . 249--289
Shaz Qadeer and
Serdar Tasiran Runtime verification of
concurrency-specific correctness
criteria . . . . . . . . . . . . . . . . 291--305
Eric Bodden and
Laurie Hendren The Clara framework for hybrid typestate
analysis . . . . . . . . . . . . . . . . 307--326
Xiaowan Huang and
Justin Seyster and
Sean Callanan and
Ketan Dixit and
Radu Grosu and
Scott A. Smolka and
Scott D. Stoller and
Erez Zadok Software monitoring with controllable
overhead . . . . . . . . . . . . . . . . 327--347
Yli\`es Falcone and
Jean-Claude Fernandez and
Laurent Mounier What can you verify and enforce at
runtime? . . . . . . . . . . . . . . . . 349--382
Alexandre Petrenko and
Adenilso Simao and
José Carlos Maldonado Model-based testing of software and
systems: recent advances and challenges 383--386
Margus Veanes and
Nikolaj Bjòrner Alternating simulation and IOCO . . . . 387--405
Yli\`es Falcone and
Jean-Claude Fernandez and
Thierry Jéron and
Hervé Marchand and
Laurent Mounier More testable properties . . . . . . . . 407--437
Christoph D. Gladisch Model generation for quantified formulas
with application to test data generation 439--459
Silvia Regina Vergilio and
Aurora Pozo and
João Carlos Garcia Árias and
Rafael da Veiga Cabral and
Tiago Nobre Multi-objective optimization algorithms
applied to the class integration and
test order problem . . . . . . . . . . . 461--475
Ina Schaefer and
Rick Rabiser and
Dave Clarke and
Lorenzo Bettini and
David Benavides and
Goetz Botterweck and
Animesh Pathak and
Salvador Trujillo and
Karina Villela Software diversity: state of the art and
perspectives . . . . . . . . . . . . . . 477--495
Andreas Pleuss and
Goetz Botterweck Visualization of variability and
configuration options . . . . . . . . . 497--510
Sven Jörges and
Anna-Lena Lamprecht and
Tiziana Margaria and
Ina Schaefer and
Bernhard Steffen A constraint-based variability modeling
framework . . . . . . . . . . . . . . . 511--530
Reinhard Tartler and
Julio Sincero and
Christian Dietrich and
Wolfgang Schröder-Preikschat and
Daniel Lohmann Revealing and repairing configuration
inconsistencies in large-scale system
software . . . . . . . . . . . . . . . . 531--551
Patrick Heymans and
Quentin Boucher and
Andreas Classen and
Arnaud Bourdoux and
Laurent Demonceau A code tagging approach to software
product line development: an application
to satellite communication libraries . . 553--566
Peter Y. H. Wong and
Elvira Albert and
Radu Muschevici and
José Proença and
Jan Schäfer and
Rudolf Schlatte The ABS tool suite: modelling, executing
and analysing distributed adaptable
object-oriented systems . . . . . . . . 567--588
Andreas Classen and
Maxime Cordy and
Patrick Heymans and
Axel Legay and
Pierre-Yves Schobbens Model checking software product lines
with SNIP . . . . . . . . . . . . . . . 589--612
Wolfgang Heider and
Rick Rabiser and
Paul Grünbacher Facilitating the evolution of products
in product line engineering by capturing
and replaying configuration decisions 613--630
Zhiming Liu and
Abhik Roychoudhury Relating software validation to
technology trends . . . . . . . . . . . 631--638
Minxue Pan and
Xuandong Li Timing analysis of MSC specifications
with asynchronous concatenation . . . . 639--651
Chunqing Chen and
Jun Sun and
Yang Liu and
Jin Song Dong and
Manchun Zheng Formal modeling and validation of
Stateflow diagrams . . . . . . . . . . . 653--671
Adriano Gomes and
Alexandre Mota and
Augusto Sampaio and
Felipe Ferri and
Edson Watanabe Constructive model-based analysis for
safety assessment . . . . . . . . . . . 673--702
Alexandre David and
Kim. G. Larsen and
Axel Legay and
Mikael H. Mòller and
Ulrik Nyman and
Anders P. Ravn and
Arne Skou and
Andrzej W\kasowski Compositional verification of real-time
systems using Ecdar . . . . . . . . . . 703--720
Björn Lisper The ALL-TIMES project: introduction and
overview . . . . . . . . . . . . . . . . 1--8
Nicholas Merriam and
Peter Gliwa and
Ian Broster Measurement and tracing methods for
timing analysis . . . . . . . . . . . . 9--28
Reinhold Heckmann and
Christian Ferdinand and
Daniel Kästner and
Stefana Nenova Architecture exploration and timing
estimation during early design phases 29--39
Dietmar Schreiner and
Gergö Barany and
Markus Schordan and
Jens Knoop Comparison of type-based and alias-based
component recognition for embedded
systems software . . . . . . . . . . . . 41--52
Björn Lisper and
Andreas Ermedahl and
Dietmar Schreiner and
Jens Knoop and
Peter Gliwa Practical experiences of applying
source-level WCET flow analysis to
industrial code . . . . . . . . . . . . 53--63
Nicholas Merriam and
Björn Lisper Estimation of productivity increase for
timing analysis tool chains . . . . . . 65--84
Parosh Aziz Abdulla and
K. Rustan M. Leino Tools for software verification . . . . 85--88
Hubert Garavel and
Frédéric Lang and
Radu Mateescu and
Wendelin Serwe CADP 2011: a toolbox for the
construction and analysis of distributed
processes . . . . . . . . . . . . . . . 89--107
Yih-Kuen Tsay and
Ming-Hsien Tsai and
Jinn-Shu Chang and
Yi-Wen Chang and
Chi-Shiang Liu Büchi Store: an open repository of $
\omega $-automata . . . . . . . . . . . 109--123
Abinoam P. Marques Jr. and
Anders P. Ravn and
Jirí Srba and
Saleem Vighio Model-checking Web services business
activity protocols . . . . . . . . . . . 125--147
Saddek Bensalem and
Axel Legay and
Marius Bozga Rigorous embedded design: challenges and
perspectives . . . . . . . . . . . . . . 149--154
Kai Lampka and
Simon Perathoner and
Lothar Thiele Component-based system design: analytic
real-time interfaces for state-based
component implementations . . . . . . . 155--170
Jonas Rox and
Rolf Ernst Compositional performance analysis with
improved analysis techniques for
obtaining viable end-to-end latencies in
distributed embedded systems . . . . . . 171--187
Silviu S. Craciunas and
Christoph M. Kirsch and
Hannes Payer and
Harald Röck and
Ana Sokolova Temporal isolation in real-time systems:
the VBS approach . . . . . . . . . . . . 189--209
Thi Thieu Hoa Le and
Luigi Palopoli and
Roberto Passerone and
Yusi Ramadian Timed-automata based schedulability
analysis for distributed firm real-time
systems: a case study . . . . . . . . . 211--228
Ismail Assayad and
Alain Girault and
Hamoudi Kalla Tradeoff exploration between
reliability, power consumption, and
execution time for embedded systems . . 229--245
Oded Maler and
Dejan Nickovi\'c Monitoring properties of analog and
mixed-signal circuits . . . . . . . . . 247--268
Fred Houben and
Georgeta Igna and
Frits Vaandrager Modeling task systems using
parameterized partial orders . . . . . . 269--286
Stefan Kowalewski and
Anna Philippou and
Jörg Brauer Model checking and abstract
interpretation as building blocks of
advanced program analysis techniques . . 287--289
Ashutosh Kumar Gupta and
Rupak Majumdar and
Andrey Rybalchenko From tests to proofs . . . . . . . . . . 291--303
Erion Plaku and
Lydia E. Kavraki and
Moshe Y. Vardi Falsification of LTL safety properties
in hybrid systems . . . . . . . . . . . 305--320
Vineet Kahlon and
Sriram Sankaranarayanan and
Aarti Gupta Static analysis for concurrent programs
with applications to data race detection 321--336
Viet Yen Nguyen and
Theo C. Ruys Selected dynamic issues in software
model checking . . . . . . . . . . . . . 337--362
Massimo Bombino and
Patrizia Scandurra A model-driven co-simulation environment
for heterogeneous systems . . . . . . . 363--374
Islam Abdelhalim and
Steve Schneider and
Helen Treharne An integrated framework for checking the
behaviour of fUML models using CSP . . . 375--396
Rastislav Bodik and
Barbara Jobstmann Algorithmic program synthesis:
introduction . . . . . . . . . . . . . . 397--411
Martin Vechev and
Eran Yahav and
Greta Yorsh Abstraction-guided synthesis of
synchronization . . . . . . . . . . . . 413--431
Saqib Sohail and
Fabio Somenzi Safety first: a two-stage algorithm for
the synthesis of reactive systems . . . 433--454
Viktor Kuncak and
Mikaël Mayer and
Ruzica Piskac and
Philippe Suter Functional synthesis for linear
arithmetic and sets . . . . . . . . . . 455--474
Armando Solar-Lezama Program sketching . . . . . . . . . . . 475--495
Saurabh Srivastava and
Sumit Gulwani and
Jeffrey S. Foster Template-based program verification and
program synthesis . . . . . . . . . . . 497--518
Bernd Finkbeiner and
Sven Schewe Bounded synthesis . . . . . . . . . . . 519--539
Emmanuel Filiot and
Naiyong Jin and
Jean-François Raskin Exploiting structure in LTL synthesis 541--561
Robert Könighofer and
Georg Hofferek and
Roderick Bloem Debugging formal specifications: a
practical approach using model-based
diagnosis and counterstrategies . . . . 563--583
Yashdeep Godhal and
Krishnendu Chatterjee and
Thomas A. Henzinger Synthesis of AMBA AHB from formal
specification: a case study . . . . . . 585--601
Yoad Lustig and
Moshe Y. Vardi Synthesis from component libraries . . . 603--618
Saddek Bensalem and
Klaus Havelund and
Andrea Orlandini Verification and validation meet
planning and scheduling . . . . . . . . 1--12
Robert P. Goldman and
Michael J. S. Pelican and
David J. Musliner A loop acceleration technique to speed
up verification of automatically
generated plans . . . . . . . . . . . . 13--29
Jason Crampton and
Michael Huth and
Jim Huan-Pu Kuo Authorized workflow schemas: deciding
realizability through $ \mathsf
{LTL}(\mathsf {F}) $ model checking . . 31--48
Niloofar Razavi and
Azadeh Farzan and
Sheila A. McIlraith Generating effective tests for
concurrent programs via AI automated
planning techniques . . . . . . . . . . 49--65
Jason Snyder and
Deepan Seeralan and
Shereef Sayed and
Jeffery Wilson and
Carl B. Dietrich and
Stephen H. Edwards and
Jeffrey H. Reed Open source software-defined radio tools
for education, research, and rapid
prototyping . . . . . . . . . . . . . . 67--80
Jan Tobias Mühlberg and
Gerald Lüttgen Symbolic object code analysis . . . . . 81--102
Hél\`ene Collavizza and
Nguyen Le Vinh and
Olivier Ponsini and
Michel Rueher and
Antoine Rollet Constraint-based BMC: a backjumping
strategy . . . . . . . . . . . . . . . . 103--121
Cormac Flanagan and
Barbara König Developments in automated verification
techniques . . . . . . . . . . . . . . . 123--125
Ahmed Bouajjani and
Michael Emmi Bounded phase analysis of
message-passing programs . . . . . . . . 127--146
Fu Song and
Tayssir Touili Pushdown model checking for malware
detection . . . . . . . . . . . . . . . 147--173
Arlen Cox and
Sriram Sankaranarayanan and
Bor-Yuh Evan Chang A bit too precise? Verification of
quantized digital filters . . . . . . . 175--190
Zhihao Jiang and
Miroslav Pajic and
Rajeev Alur and
Rahul Mangharam Closed-loop verification of medical
devices with model abstraction and
refinement . . . . . . . . . . . . . . . 191--213
Jens Grabowski and
Ina Schieferdecker and
Andreas Ulrich History, status, and recent trends of
the testing and test control notation
version 3 (TTCN-3) . . . . . . . . . . . 215--225
Philip Makedonski and
Jens Grabowski and
Florian Philipp Quantifying the evolution of TTCN-3 as a
language . . . . . . . . . . . . . . . . 227--246
Juergen Grossmann Testing hybrid systems with TTCN-3
embedded . . . . . . . . . . . . . . . . 247--267
Bernard Stepien and
Liam Peyton Innovation and evolution in integrated
web application testing with TTCN-3 . . 269--283
Benjamin Zeiss and
Andras Kovacs and
Nikolay Pakulin and
Bogdan Stanca-Kaposta A conformance test suite for TTCN-3
tools . . . . . . . . . . . . . . . . . 285--294
Thomas Rings and
Patrick Poglitsch and
Stephan Schulz and
Luca Serazio and
Theofanis Vassiliou-Gioles A generic interoperability testing
framework and a systematic development
process for automated interoperability
testing . . . . . . . . . . . . . . . . 295--313
Awny Alnusair and
Tian Zhao and
Gongjun Yan Rule-based detection of design patterns
in program code . . . . . . . . . . . . 315--334
Tiziana Margaria and
Zongyan Qiu and
Hongli Yang Program verification and testing
technologies . . . . . . . . . . . . . . 335--337
Huixing Fang and
Jianqi Shi and
Huibiao Zhu and
Jian Guo and
Kim Guldstrand Larsen and
Alexandre David Formal verification and simulation for
platform screen doors and collision
avoidance in subway control systems . . 339--361
Cristian Gherghina and
Cristina David and
Shengchao Qin and
Wei-Ngan Chin Expressive program verification via
structured specifications . . . . . . . 363--380
João F. Ferreira and
Cristian Gherghina and
Guanhua He and
Shengchao Qin and
Wei-Ngan Chin Automated verification of the FreeRTOS
scheduler in Hip/Sleek . . . . . . . . . 381--397
Yosr Jarraya and
Mourad Debbabi Quantitative and qualitative analysis of
SysML activity diagrams . . . . . . . . 399--419
Ender Yüksel and
Hanne Riis Nielson and
Flemming Nielson and
Huibiao Zhu and
Heqing Huang Quantitative modelling and analysis of a
Chinese smart grid: a stochastic model
checking case study . . . . . . . . . . 421--435
Hai-Feng Guo and
Mahadevan Subramaniam Model-based test generation using
extended symbolic grammars . . . . . . . 437--455
Falk Howar and
Malte Isberner and
Maik Merten and
Bernhard Steffen and
Dirk Beyer and
Corina S. Pasareanu Rigorous examination of reactive systems 457--464
Bernhard Steffen and
Malte Isberner and
Stefan Naujokat and
Tiziana Margaria and
Maren Geske Property-driven benchmark generation:
synthesizing programs of realistic
structure . . . . . . . . . . . . . . . 465--479
Jaco van de Pol and
Theo C. Ruys and
Steven te Brinke Thoughtful brute-force attack of the
RERS 2012 and 2013 Challenges . . . . . 481--491
Markus Schordan and
Adrian Prantl Combining static analysis and state
transition graphs for verification of
event-condition-action systems in the
RERS 2012 and 2013 Challenges . . . . . 493--505
Dirk Beyer and
Andreas Stahlbauer BDD-based software verification . . . . 507--518
Jeremy Morse and
Lucas Cordeiro and
Denis Nicole and
Bernd Fischer Applying symbolic bounded model checking
to the 2012 RERS Greybox Challenge . . . 519--529
Oliver Bauer and
Maren Geske and
Malte Isberner Analyzing program behavior through
active automata learning . . . . . . . . 531--542
Bernhard Steffen and
Falk Howar and
Malte Isberner and
Stefan Naujokat and
Tiziana Margaria Tailored generation of concurrent
benchmarks . . . . . . . . . . . . . . . 543--558
Michael Felderer and
Ina Schieferdecker A taxonomy of risk-based testing . . . . 559--568
Johannes Neubauer and
Stephan Windmüller and
Bernhard Steffen Risk-based testing via active continuous
quality control . . . . . . . . . . . . 569--591
Gabriella Carrozza and
Roberto Pietrantuono and
Stefano Russo Dynamic test planning: a study in an
industrial context . . . . . . . . . . . 593--607
Michael Felderer and
Rudolf Ramler A multiple case study on risk-based
testing in industry . . . . . . . . . . 609--625
Gencer Erdogan and
Yan Li and
Ragnhild Kobro Runde and
Fredrik Seehusen and
Ketil Stòlen Approaches for the combined use of risk
analysis and testing: a systematic
literature review . . . . . . . . . . . 627--642
Alessandro Fantechi and
Francesco Flammini and
Stefania Gnesi Formal methods for railway control
systems . . . . . . . . . . . . . . . . 643--646
Alessio Ferrari and
Giorgio O. Spagnolo and
Giacomo Martelli and
Simone Menabeni From commercial documents to system
requirements: an approach for the
engineering of novel CBTC solutions . . 647--667
Stefano Marrone and
Francesco Flammini and
Nicola Mazzocca and
Roberto Nardone and
Valeria Vittorini Towards Model-Driven V&V assessment of
railway control systems . . . . . . . . 669--683
Phillip James and
Faron Moller and
Hoang Nga Nguyen and
Markus Roggenbach and
Steve Schneider and
Helen Treharne Techniques for modelling and verifying
railway interlockings . . . . . . . . . 685--711
Anne E. Haxthausen Automated generation of formal safety
conditions from railway interlocking
tables . . . . . . . . . . . . . . . . . 713--726
Stefan J. Galler and
Bernhard K. Aichernig Survey on test data generation tools . . 727--751
Stefano Quer Model checking evaluation of airplane
landing trajectories . . . . . . . . . . 753--773
Agneta Nilsson and
Laura M. Castro and
Samuel Rivas and
Thomas Arts Assessing the effects of introducing a
new software development process: a
methodological description . . . . . . . 1--16
Alexandre David and
Kim G. Larsen and
Axel Legay and
Ulrik Nyman and
Louis-Marie Traonouez and
Andrzej Wasowski Real-time specifications . . . . . . . . 17--45
Hong Yi Chen and
Shaked Flur and
Supratik Mukhopadhyay Termination proofs for linear simple
loops . . . . . . . . . . . . . . . . . 47--57
Muhammad Shafique and
Yvan Labiche A systematic review of state-based test
tools . . . . . . . . . . . . . . . . . 59--76
Reza Pulungan and
Holger Hermanns A construction and minimization service
for continuous probability distributions 77--90
Daniel Lincke and
Sibylle Schupp and
Cezar Ionescu Functional prototypes for generic C++
libraries: a transformational approach
based on higher-order, typed signatures 91--105
Peter Y. H. Wong and
Richard Bubel and
Frank S. de Boer and
Miguel Gómez-Zamalloa and
Stijn de Gouw and
Reiner Hähnle and
Karl Meinke and
Muddassar Azam Sindhu Testing abstract behavioral
specifications . . . . . . . . . . . . . 107--119
Yli\`es Falcone and
Lenore D. Zuck Runtime verification: the application
perspective . . . . . . . . . . . . . . 121--123
Sylvain Hallé and
Jason Vallet and
Raphaël Tremblay-Lessard On piggyback runtime monitoring of
object-oriented programs . . . . . . . . 125--142
Klaus Havelund Rule-based runtime verification
revisited . . . . . . . . . . . . . . . 143--170
Ayoub Nouri and
Saddek Bensalem and
Marius Bozga and
Benoit Delahaye and
Cyrille Jegourel and
Axel Legay Statistical model checking QoS
properties of systems with SBIP . . . . 171--185
Alexandre David and
Kim G. Larsen and
Axel Legay and
Marius Mikucionis Schedulability of Herschel revisited
using statistical model checking . . . . 187--199
Sébastien Salva and
Stassia R. Zafimiharisoa APSET, an Android aPplication SEcurity
Testing tool for detecting intent-based
vulnerabilities . . . . . . . . . . . . 201--221
Farn Wang Model-checking fair dense-time systems
with propositions and events . . . . . . 223--243
Michael Felderer and
Basel Katt A process for mastering security
evolution in the development lifecycle 245--250
Atle Refsdal and
Bjòrnar Solhaug and
Ketil Stòlen Security risk analysis of system changes
exemplified within the oil and gas
domain . . . . . . . . . . . . . . . . . 251--266
Jens Bürger and
Jan Jürjens and
Sven Wenzel Restoring security of evolving software
models using graph transformation . . . 267--289
Dries Vanoverberghe and
Frank Piessens Policy ignorant caller-side inline
reference monitoring . . . . . . . . . . 291--303
Michael Felderer and
Elizabeta Fourneret A systematic classification of security
regression testing approaches . . . . . 305--319
Kenneth J. Turner and
Paul S. Lambert Workflows for quantitative data analysis
in the social sciences . . . . . . . . . 321--338
Grzegorz Anielak and
Grzegorz Jakacki and
Slawomir Lasota Incremental test case generation using
bounded model checking: an application
to automatic rating . . . . . . . . . . 339--349
Alexandre David and
Kim G. Larsen and
Axel Legay and
Marius Mikucionis and
Danny Bògsted Poulsen and
Sean Sedwards Statistical model checking for
biological systems . . . . . . . . . . . 351--367
Axel Legay and
Mahesh Viswanathan Statistical model checking: challenges
and perspectives . . . . . . . . . . . . 369--376
Daniël Reijsbergen and
Pieter-Tjerk de Boer and
Werner Scheinhardt and
Boudewijn Haverkort On hypothesis testing for statistical
model checking . . . . . . . . . . . . . 377--395
Alexandre David and
Kim G. Larsen and
Axel Legay and
Marius Mikucionis and
Danny Bògsted Poulsen Uppaal SMC tutorial . . . . . . . . . . 397--415
Nima Roohi and
Mahesh Viswanathan Statistical model checking for unbounded
until formulas . . . . . . . . . . . . . 417--427
Arnd Hartmanns and
Mark Timmer Sound statistical model checking for MDP
using partial order and confluence
reduction . . . . . . . . . . . . . . . 429--456
Richard Lassaigne and
Sylvain Peyronnet Approximate planning and verification
for large Markov decision processes . . 457--467
Pedro D'Argenio and
Axel Legay and
Sean Sedwards and
Louis-Marie Traonouez Smart sampling for lightweight
verification of Markov decision
processes . . . . . . . . . . . . . . . 469--484
Christian Ellen and
Sebastian Gerwinn and
Martin Fränzle Statistical model checking for
stochastic hybrid systems involving
nondeterminism over continuous domains 485--504
Paolo Ballarini Analysing oscillatory trends of
discrete-state stochastic processes
through HASL statistical model checking 505--526
Paolo Zuliani Statistical model checking for
biological applications . . . . . . . . 527--536
Souymodip Chakraborty and
Joost-Pieter Katoen and
Falak Sher and
Martin Strelec Modelling and statistical model checking
of a microgrid . . . . . . . . . . . . . 537--554
Stefania Gnesi and
Stan Jarzabek Special section on the 17th
International Software Product Line
Conference . . . . . . . . . . . . . . . 555--557
Holger Eichelberger and
Klaus Schmid Mapping the design-space of textual
variability modeling languages: a
refined analysis . . . . . . . . . . . . 559--584
João Bosco Ferreira Filho and
Olivier Barais Generating counterexamples of
model-based software product lines . . . 585--600
Arne Haber and
Katrin Hölldobler Systematic synthesis of delta modeling
languages . . . . . . . . . . . . . . . 601--626
Julia Rubin and
Krzysztof Czarnecki Cloned product variants: from ad-hoc to
managed software product lines . . . . . 627--646
Marieke Huisman and
Vladimir Klebanov VerifyThis 2012 . . . . . . . . . . . . 647--657
Bart Jacobs and
Jan Smans and
Frank Piessens Solving the VerifyThis 2012 challenges
with VeriFast . . . . . . . . . . . . . 659--676
Gidon Ernst and
Jörg Pfähler KIV: overview and VerifyThis competition 677--694
Duc Hoang and
Yannick Moy and
Angela Wallenburg SPARK 2014 and GNATprove . . . . . . . . 695--707
François Bobot and
Jean-Christophe Filliâtre Let's verify this with Why3 . . . . . . 709--727
Daniel Bruns and
Wojciech Mostowski Implementation-level verification of
algorithms with KeY . . . . . . . . . . 729--744
Julian Tschannen and
Carlo A. Furia AutoProof meets some verification
challenges . . . . . . . . . . . . . . . 745--755
Stefan Blom and
Marieke Huisman Witnessing the elimination of magic
wands . . . . . . . . . . . . . . . . . 757--781
Mauro Pezzé and
Jochen Wuttke Model-driven generation of runtime
checks for system properties . . . . . . 1--19
Martijn Hendriks and
Twan Basten A blueprint for system-level performance
modeling of software-intensive embedded
systems . . . . . . . . . . . . . . . . 21--40
Martin Wehrle and
Sebastian Kupferschmid Downward pattern refinement for timed
automata . . . . . . . . . . . . . . . . 41--56
Takeru Inoue and
Hiroaki Iwashita and
Jun Kawahara Graphillion: software library for very
large sets of labeled graphs . . . . . . 57--66
Jan-David Quesel and
Stefan Mitsch and
Sarah Loos How to model and prove hybrid systems
with \pkgKeYmaera: a tutorial on safety 67--91
Ammar Osaiweran and
Mathijs Schuts Evaluating the effect of a lightweight
formal technique in industry . . . . . . 93--108
Takuro Kutsuna and
Yoshinao Ishii Abstraction and refinement of
mathematical functions toward SMT-based
test-case generation . . . . . . . . . . 109--120
Erika Ábrahám and
Klaus Havelund Some recent advances in automated
analysis . . . . . . . . . . . . . . . . 121--128
Gavin Lowe Concurrent depth-first search algorithms
based on Tarjan's Algorithm . . . . . . 129--147
Thomas Gibson-Robinson and
Philip Armstrong FDR3: a parallel refinement checker for
CSP . . . . . . . . . . . . . . . . . . 149--167
Anton Wijs and
Dragan Bosnacki Many-core on-the-fly model checking of
safety properties using GPUs . . . . . . 169--185
Alessandro Armando and
Roberto Carbone SATMC: a SAT-based model checker for
security protocols, business processes,
and security APIs . . . . . . . . . . . 187--204
Normann Decker and
Martin Leucker and
Daniel Thoma Monitoring modulo theories . . . . . . . 205--225
Christian von Essen and
Dimitra Giannakopoulou Probabilistic verification and synthesis
of the next generation airborne
collision avoidance system . . . . . . . 227--243
Hüsnü Yenigün and
Cemal Yilmaz and
Andreas Ulrich Advances in test generation for testing
software and systems . . . . . . . . . . 245--249
Natalia Kushik and
Khaled El-Fakih and
Nina Yevtushenko and
Ana R. Cavalli On adaptive experiments for
nondeterministic finite state machines 251--264
Wen-ling Huang and
Jan Peleska Complete model-based equivalence class
testing . . . . . . . . . . . . . . . . 265--283
João Pascoal Faria and
Ana C. R. Paiva A toolset for conformance testing
against UML sequence diagrams based on
event-driven colored Petri nets . . . . 285--304
Hernán Ponce de León and
Stefan Haar and
Delphine Longuet Model-based testing for concurrent
systems: unfolding-based test selection 305--318
Peter Schrammel and
Tom Melham and
Daniel Kroening Generating test case chains for reactive
systems . . . . . . . . . . . . . . . . 319--334
Eduard P. Enoiu and
Adnan Causevi\'c and
Thomas J. Ostrand and
Elaine J. Weyuker and
Daniel Sundmark and
Paul Pettersson Automated test generation using model
checking: an industrial evaluation . . . 335--353
Ezio Bartocci and
C. R. Ramakrishnan Preface of the special issue on Model
Checking of Software . . . . . . . . . . 355--357
Nuno P. Lopes and
José Monteiro Automatic equivalence checking of
programs with uninterpreted functions
and integer arithmetic . . . . . . . . . 359--374
Divjyot Sethi and
Muralidhar Talupur and
Sharad Malik Model checking unbounded concurrent
lists . . . . . . . . . . . . . . . . . 375--391
Kiran Adhikari and
James Street and
Chao Wang and
Yang Liu and
Shaojie Zhang Verifying a quantitative relaxation of
linearizability via refinement . . . . . 393--407
Jonas Finnemann Jensen and
Kim Guldstrand Larsen and
Jirí Srba and
Lars Kaerlund Oestergaard Efficient model-checking of weighted CTL
with upper-bound constraints . . . . . . 409--426
Alfons Laarman and
Elwin Pater and
Jaco van de Pol and
Henri Hansen Guard-based partial-order reduction . . 427--448
Sergiy Bogomolov and
Alexandre Donzé and
Goran Frehse and
Radu Grosu and
Taylor T. Johnson and
Hamed Ladan and
Andreas Podelski and
Martin Wehrle Guided search for hybrid systems based
on coarse-grained space abstractions . . 449--467
Parosh A. Abdulla and
Giorgio Delzanno Parameterized verification . . . . . . . 469--473
Giorgio Delzanno A unified view of parameterized
verification of abstract models of
broadcast communication . . . . . . . . 475--493
Parosh Abdulla and
Frédéric Haziza and
Lukás Holík Parameterized verification through view
abstraction . . . . . . . . . . . . . . 495--516
Zeinab Ganjei and
Ahmed Rezine and
Petru Eles and
Zebo Peng Counting dynamically synchronizing
processes . . . . . . . . . . . . . . . 517--534
Marco Montali and
Diego Calvanese Soundness of data-aware, case-centric
processes . . . . . . . . . . . . . . . 535--558
Silvio Ranise and
Anh Truong and
Riccardo Traverso Parameterized model checking for
security policy analysis . . . . . . . . 559--573
Anna-Lena Lamprecht and
Kenneth J. Turner Scientific workflows . . . . . . . . . . 575--580
Hervé Ménager and
Matús Kalas and
Kristoffer Rapacki and
Jon Ison Using registries to integrate
bioinformatics tools and services into
workbench environments . . . . . . . . . 581--586
R. O. Sinnott and
W. Voorsluys A scalable cloud-based system for
data-intensive spatial analysis . . . . 587--605
Alfredo Bolt and
Massimiliano de Leoni and
Wil M. P. van der Aalst Scientific workflows for process mining:
building blocks, scenarios, and
implementation . . . . . . . . . . . . . 607--628
Anna-Lena Lamprecht and
Bernhard Steffen and
Tiziana Margaria Scientific workflows with the jABC
framework . . . . . . . . . . . . . . . 629--651
Afshin Amighi and
Pedro de Carvalho Gomes and
Dilian Gurov and
Marieke Huisman Provably correct control flow graphs
from Java bytecode programs with
exceptions . . . . . . . . . . . . . . . 653--684
Amar Kumar Gupta and
Guy Edward Gallasch Equivalence class verification of the
contract net protocol-extension . . . . 685--706
Bernhard Steffen The physics of software tools: SWOT
analysis and vision . . . . . . . . . . 1--7
Alessio Lomuscio and
Hongyang Qu and
Franco Raimondi MCMAS: an open-source model checker for
the verification of multi-agent systems 9--30
Víctor Rivera and
Néstor Cataño and
Tim Wahls and
Camilo Rueda Code generation for Event-B . . . . . . 31--52
Adriana C. Damasceno and
Patricia D. L. Machado and
Wilkerson L. Andrade Testing real-time systems from
compositional symbolic specifications 53--71
Kangfeng Ye and
Jim Woodcock Model checking of state-rich formalism
by linking to CSP\,$ \Vert $ \,B . . . . 73--96
Mikhail Y. R. Gadelha and
Hussama I. Ismail and
Lucas C. Cordeiro Handling loops in bounded model checking
of C programs via $k$-induction . . . . 97--114
Philipp Zech and
Philipp Kalb and
Michael Felderer and
Colin Atkinson and
Ruth Breu Model-based regression testing by OCL 115--131
Frédéric Boniol and
Virginie Wiels and
Yamine A\"\it-Ameur and
Klaus-Dieter Schewe The landing gear case study: challenges
and experiments . . . . . . . . . . . . 133--140
Wen Su and
Jean-Raymond Abrial Aircraft landing gear system: approaches
with Event-B to the modeling of an
industrial system . . . . . . . . . . . 141--166
Amel Mammar and
Régine Laleau Modeling a landing gear system in
Event-B . . . . . . . . . . . . . . . . 167--186
Lukas Ladenberger and
Dominik Hansen and
Harald Wiegard and
Jens Bendisposto and
Michael Leuschel Validation of the ABZ landing gear
system using ProB . . . . . . . . . . . 187--203
Richard Banach The landing gear system in multi-machine
Hybrid Event-B . . . . . . . . . . . . . 205--228
Ciprian Teodorov and
Philippe Dhaussy and
Luka Le Roux Environment-driven reachability for
timed systems . . . . . . . . . . . . . 229--245
Paolo Arcaini and
Angelo Gargantini and
Elvinia Riccobene Rigorous development process of a
safety-critical system: from ASM models
to Java code . . . . . . . . . . . . . . 247--269
Steffen Herbold and
Andreas Hoffmann Model-based testing as a service . . . . 271--279
Lom Messan Hillah and
Ariele-Paolo Maesano and
Fabio De Rosa and
Fabrice Kordon and
Pierre-Henri Wuillemin and
Riccardo Fontanelli and
Sergio Di Bona and
Davide Guerri and
Libero Maesano Automation and intelligent scheduling of
distributed system functional testing 281--308
Steffen Herbold and
Patrick Harms and
Jens Grabowski Combining usage-based and model-based
testing for service-oriented
architectures in the industrial practice 309--324
M. A. Barcelona and
L. García-Borgoñón and
G. López-Nicolás Practical experiences in the usage of
MIDAS in the logistics domain . . . . . 325--339
Yli\`es Falcone and
Mohamad Jaber Fully automated runtime enforcement of
component-based systems with formal and
sound recovery . . . . . . . . . . . . . 341--365
Swen Jacobs and
Roderick Bloem and
Romain Brenguier and
Rüdiger Ehlers and
Timotheus Hell and
Robert Könighofer and
Guillermo A. Pérez and
Jean-François Raskin and
Leonid Ryzhyk and
Ocan Sankur and
Martina Seidl and
Leander Tentrup and
Adam Walker The first reactive synthesis competition
(SYNTCOMP 2014) . . . . . . . . . . . . 367--390
Matthias Güdemann and
Manuel Núñez Preface of the special issue on formal
methods in industrial critical systems 391--393
Bogdan Aman and
Gabriel Ciobanu Verification of critical systems
described in real-time TiMo . . . . . . 395--408
Bernhard K. Aichernig and
Klaus Hörmaier and
Florian Lorber and
Dejan Nickovi\'c and
Stefan Tiran Require, test, and trace IT . . . . . . 409--426
Nasrine Damouche and
Matthieu Martel and
Alexandre Chapoutot Improving the numerical accuracy of
programs by automatic transformation . . 427--448
Gal Katz and
Doron Peled Synthesizing, correcting and improving
code, using model checking-based genetic
programming . . . . . . . . . . . . . . 449--464
Zoubeyr Farah and
Yamine Ait-Ameur and
Meriem Ouederni and
Kamel Tari A correct-by-construction model for
asynchronously communicating systems . . 465--485
Martijn Hendriks and
Jacques Verriet and
Twan Basten and
Bart Theelen and
Marco Brassé and
Lou Somers Analyzing execution traces:
critical-path analysis and distance
analysis . . . . . . . . . . . . . . . . 487--510
Nir Piterman Advances in verification presented in
TACAS'13 . . . . . . . . . . . . . . . . 511--515
Grigory Fedyukovich and
Ondrej Sery and
Natasha Sharygina Flexible SAT-based framework for
incremental bounded upgrade checking . . 517--534
Isil Dillig and
Thomas Dillig and
Boyang Li and
Ken McMillan and
Mooly Sagiv Synthesis of circular compositional
program proofs via abduction . . . . . . 535--547
Parosh Aziz Abdulla and
Frédéric Haziza and
Lukás Holík and
Bengt Jonsson and
Ahmed Rezine An integrated specification and
verification technique for highly
concurrent data structures for highly
concurrent data structures . . . . . . . 549--563
Pierre Ganty and
Radu Iosif and
Filip Konecný Underapproximation of procedure
summaries for integer programs . . . . . 565--584
Aleksandar S. Dimovski and
Ahmad Salim Al-Sibahi and
Claus Brabrand and
Andrzej Wasowski Efficient family-based model checking
via variability abstractions . . . . . . 585--603
Heinz Riener and
Finn Haedicke and
Stefan Frehse and
Mathias Soeken and
Daniel Große and
Rolf Drechsler and
Goerschwin Fey metaSMT: focus on your application and
not on solver integration . . . . . . . 605--621
Tatsuya Abe and
Toshiyuki Maeda A general model checking framework for
various memory consistency models . . . 623--647
Christel Baier and
Cesare Tinelli Some advances in tools and algorithms
for the construction and analysis of
systems . . . . . . . . . . . . . . . . 649--652
E. Renault and
A. Duret-Lutz and
F. Kordon and
D. Poitrenaud Variations on parallel explicit
emptiness checks for generalized Büchi
automata . . . . . . . . . . . . . . . . 653--673
Tom van Dijk and
Jaco van de Pol Sylvan: multi-core framework for
decision diagrams . . . . . . . . . . . 675--696
Carlo A. Furia and
Martin Nordio and
Nadia Polikarpova and
Julian Tschannen AutoProof: auto-active functional
verification of object-oriented programs 697--716
Jean-Baptiste Jeannin and
Khalil Ghorbal and
Yanni Kouskoulas and
Aurora Schmidt and
Ryan Gardner and
Stefan Mitsch and
André Platzer A formally verified hybrid system for
safe advisories in the next-generation
airborne collision avoidance system . . 717--741
Reza Meimandi Parizi and
Abdul Azim Abdul Ghani and
Sai Peck Lee and
Saif Ur Rehman Khan RAMBUTANS: automatic AOP-specific test
generation tool . . . . . . . . . . . . 743--761
Marieke Huisman and
Vladimir Klebanov and
Rosemary Monahan and
Michael Tautschnig VerifyThis 2015 . . . . . . . . . . . . 763--771
Mohamad Jaber and
Yli\`es Falcone and
Kinan Dak-Al-Bab and
John Abou-Jaoudeh and
Mostafa El-Katerji A high-level modeling language for the
efficient design, implementation, and
testing of Android applications . . . . 1--18
Ily\`es Boukhari and
Stéphane Jean and
Idir Ait-Sadoune and
Ladjel Bellatreche The role of user requirements in data
repository design . . . . . . . . . . . 19--34
Vladimir Ulyantsev and
Igor Buzhinsky and
Anatoly Shalyto Exact finite-state machine
identification from scenarios and
temporal properties . . . . . . . . . . 35--55
Josie Holmes and
Alex Groce and
Jervis Pinto and
Pranjal Mittal and
Pooria Azimi and
Kevin Kellar and
James O'Brien TSTL: the template scripting testing
language . . . . . . . . . . . . . . . . 57--78
Bardh Hoxha and
Adel Dokhanchi and
Georgios Fainekos Mining parametric temporal logic
properties in model-based design for
cyber-physical systems . . . . . . . . . 79--93
Vera Pantelic and
Steven Postma and
Mark Lawford and
Monika Jaskolka and
Bennett Mackenzie and
Alexandre Korobkine and
Marc Bender and
Jeff Ong and
Gordon Marks and
Alan Wassyng Software engineering practices and
Simulink: bridging the gap . . . . . . . 95--117
Radu Mateescu Recent advances in interactive and
automated analysis . . . . . . . . . . . 119--123
Alexander Faithfull and
Jesper Bengtson and
Enrico Tassi and
Carst Tankink Coqoon . . . . . . . . . . . . . . . . . 125--137
Gudmund Grov and
Yuhui Lin The Tinker tool for graphical tactic
development . . . . . . . . . . . . . . 139--155
Tom van Dijk and
Jaco van de Pol Multi-core symbolic bisimulation
minimisation . . . . . . . . . . . . . . 157--177
Joachim Klein and
Christel Baier and
Philipp Chrszon and
Marcus Daum and
Clemens Dubslaff and
Sascha Klüppelholz and
Steffen Märcker and
David Müller Advances in probabilistic model checking
with PRISM: variable reordering,
quantiles and weak deterministic Büchi
automata . . . . . . . . . . . . . . . . 179--194
Marta Kwiatkowska and
David Parker and
Clemens Wiltsche PRISM-games: verification and strategy
synthesis for stochastic multi-player
games with multiple objectives . . . . . 195--210
Peter W. V. Tran-Jòrgensen and
Peter Gorm Larsen and
Gary T. Leavens Automated translation of VDM to
JML-annotated Java . . . . . . . . . . . 211--235
Maurice H. ter Beek and
Stefania Gnesi and
Alexander Knapp Formal methods for transport systems . . 237--241
Somsak Vanit-Anunchai Modelling and simulating a Thai railway
signalling system using Coloured Petri
Nets . . . . . . . . . . . . . . . . . . 243--262
Franco Mazzanti and
Alessio Ferrari and
Giorgio O. Spagnolo Towards formal methods diversity in
railways: an experience report with
seven frameworks . . . . . . . . . . . . 263--288
Vincenzo Ciancia and
Stephen Gilmore and
Gianluca Grilletti and
Diego Latella and
Michele Loreti and
Mieke Massink Spatio-temporal model checking of
vehicular movement in public transport
systems . . . . . . . . . . . . . . . . 289--311
G. Cabodi and
P. E. Camurati and
C. Loiacono and
M. Palena and
P. Pasini and
D. Patti and
S. Quer To split or to group: from
divide-and-conquer to sub-task sharing
for verifying multiple properties in
model checking . . . . . . . . . . . . . 313--325
Stefan Naujokat and
Michael Lybecait and
Dawid Kopetzki and
Bernhard Steffen CINCO: a simplicity-driven approach to
full generation of domain-specific
graphical modeling tools . . . . . . . . 327--354
Maurice H. ter Beek and
Stefania Gnesi and
Alexander Knapp Formal methods and automated
verification of critical systems . . . . 355--358
Johannes Leupolz and
Alexander Knapp and
Axel Habermaier and
Wolfgang Reif Qualitative and quantitative analysis of
safety-critical systems with . . . . . . 359--377
André de Matos Pedro and
Jorge Sousa Pinto and
David Pereira and
Luís Miguel Pinho Runtime verification of autopilot
systems using a fragment of MTL-$ \int $ 379--395
Mounir Chadli and
Jin H. Kim and
Kim G. Larsen and
Axel Legay and
Stefan Naujokat and
Bernhard Steffen and
Louis-Marie Traonouez High-level frameworks for the
specification and verification of
scheduling problems . . . . . . . . . . 397--422
Ning Ge and
Eric Jenn and
Nicolas Breton and
Yoann Fonteneau Integrated formal verification of
safety-critical software . . . . . . . . 423--440
Wen-ling Huang and
Jan Peleska Model-based testing strategies and their
(in)dependence on syntactic model
representations . . . . . . . . . . . . 441--465
Hadrien Bride and
Olga Kouchnarenko and
Fabien Peureux and
Guillaume Voiron Assessing SMT and CLP approaches for
workflow nets verification . . . . . . . 467--491
Dragan Bosnacki and
Anton Wijs Model checking: recent improvements and
applications . . . . . . . . . . . . . . 493--497
María del Mar Gallardo and
Pedro Merino and
Laura Panizo and
Alberto Salmerón Integrating river basin DSSs with model
checking . . . . . . . . . . . . . . . . 499--514
Stefan Edelkamp and
Christoph Greulich A case study of planning for smart
factories . . . . . . . . . . . . . . . 515--528
Peter Gjòl Jensen and
Kim Guldstrand Larsen and
Jirí Srba Discrete and continuous strategies for
timed-arc Petri net games . . . . . . . 529--546
Ehsan Khamespanah and
Marjan Sirjani and
Kirill Mechitov and
Gul Agha Modeling and analyzing real-time
wireless sensor and actuator networks
using actors and model checking . . . . 547--561
Radu Mateescu and
José Ignacio Requeno On-the-fly model checking for extended
action-based probabilistic operators . . 563--587
Antti Valmari and
Walter Vogler Fair testing and stubborn sets . . . . . 589--610
Marieke Huisman and
Julia Rubin Software quality tools and techniques
presented in FASE'17 . . . . . . . . . . 611--613
Andreas Müller and
Stefan Mitsch and
Werner Retschitzegger and
Wieland Schwinger and
André Platzer Tactical contract composition for hybrid
system component verification . . . . . 615--643
Zheng Cheng and
Massimo Tisi Slicing ATL model transformations for
scalable deductive verification and
fault localization . . . . . . . . . . . 645--663
Marcelo Uva and
Pablo Ponzio and
Germán Regis and
Nazareno Aguirre and
Marcelo F. Frias Automated workarounds from Java program
specifications based on SAT solving . . 665--688
Jingyi Wang and
Jun Sun and
Qixia Yuan and
Jun Pang Learning probabilistic models for model
checking: an evolutionary approach and
an empirical study . . . . . . . . . . . 689--704
Sven Schneider and
Leen Lambers and
Fernando Orejas Automated reasoning for attributed graph
properties . . . . . . . . . . . . . . . 705--737
Irina Mariuca Asavoae and
Mihail Asavoae and
Adrián Riesco Slicing from formal semantics: Chisel
--- a tool for generic program slicing 739--769
Dirk Beyer and
Stefan Löwe and
Philipp Wendler Reliable benchmarking: requirements and
solutions . . . . . . . . . . . . . . . 1--29
Ezio Bartocci and
Yli\`es Falcone and
Borzoo Bonakdarpour and
Christian Colombo and
Normann Decker and
Klaus Havelund and
Yogi Joshi and
Felix Klaedtke and
Reed Milewicz and
Giles Reger and
Grigore Rosu and
Julien Signoles and
Daniel Thoma and
Eugen Zalinescu and
Yi Zhang First international Competition on
Runtime Verification: rules, benchmarks,
tools, and final results of CRV 2014 . . 31--70
Andreas Fellner and
Bruno Woltzenlogel Paleo Greedy pebbling for proof space
compression . . . . . . . . . . . . . . 71--86
Stanley Bak and
Omar Ali Beg and
Sergiy Bogomolov and
Taylor T. Johnson and
Luan Viet Nguyen and
Christian Schilling Hybrid automata: from verification to
implementation . . . . . . . . . . . . . 87--104
Stanislav Dashevskyi and
Daniel Ricardo dos Santos and
Fabio Massacci and
Antonino Sabetta TestREx: a framework for repeatable
exploits . . . . . . . . . . . . . . . . 105--119
Maxime Routhier and
Richard St-Denis A qualitative assessment of $ \alpha $
Rby in the perspective of the
supervisory control theory . . . . . . . 121--141
Fadi A. Zaraket and
Mohamad Jaber and
Mohamad Noureddine and
Yli\`es Falcone From high-level modeling toward
efficient and trustworthy circuits . . . 143--163
Chunyan Fu and
Kougen Zheng Formal modeling and analysis of ad hoc
Zone Routing Protocol in Event-B . . . . 165--181
Gervasio Pérez and
Sergio Yovine Formal specification and implementation
of an automated pattern-based
parallel-code generation framework . . . 183--202
Étienne André What's decidable about parametric timed
automata? . . . . . . . . . . . . . . . 203--219
Philipp Zech and
Michael Felderer and
Ruth Breu Knowledge-based security testing of web
applications by logic programming . . . 221--246
Hakan Erdogmus and
Klaus Havelund Introduction to Selected Papers from
SPIN 2017 . . . . . . . . . . . . . . . 247--248
Jinru Hua and
Yushan Zhang and
Yuqun Zhang and
Sarfraz Khurshid EdSketch: execution-driven sketching for
Java . . . . . . . . . . . . . . . . . . 249--265
Daniel Ratiu and
Andreas Ulrich An integrated environment for Spin-based
C code checking . . . . . . . . . . . . 267--286
Michalis Kokologiannakis and
Konstantinos Sagonas Stateless model checking of the Linux
kernel's read-copy update (RCU) . . . . 287--306
Vincent Bloemen and
Alexandre Duret-Lutz and
Jaco van de Pol Model checking with generalized Rabin
and Fin-less automata . . . . . . . . . 307--324
John Fearnley and
Sanjay Jain and
Bart de Keijzer and
Sven Schewe and
Frank Stephan and
Dominik Wojtczak An ordered approach to solving parity
games in quasi-polynomial time and
quasi-linear space . . . . . . . . . . . 325--349
Esmaeel Nikravan and
Saeed Parsa A reasoning-based approach to dynamic
domain reduction in test data generation 351--364
Pavel Parízek and
Ondrej Lhoták Fast detection of concurrency errors by
state space traversal with randomization
and early backtracking . . . . . . . . . 365--400
Amit Gurung and
Rajarshi Ray and
Ezio Bartocci and
Sergiy Bogomolov and
Radu Grosu Parallel reachability analysis of hybrid
systems in XSpeed . . . . . . . . . . . 401--423
Julien Botella and
Jean-François Capuron and
Frédéric Dadeau and
Elizabeta Fourneret and
Bruno Legeard and
Florence Schadle Complementary test selection criteria
for model-based testing of security
components . . . . . . . . . . . . . . . 425--448
Simon Busard and
Charles Pecheur and
Hongyang Qu and
Franco Raimondi Comparing approaches for model-checking
strategies under imperfect information
and fairness constraints . . . . . . . . 449--469
Matthew F. Tennyson ASAP: a Source Code Authorship Program 471--484
Martin Hentschel and
Richard Bubel and
Reiner Hähnle The Symbolic Execution Debugger (SED): a
platform for interactive symbolic
execution, debugging, verification and
more . . . . . . . . . . . . . . . . . . 485--513
Martin Becker and
Ravindra Metta and
R. Venkatesh and
Samarjit Chakraborty Scalable and precise estimation and
debugging of the worst-case execution
time for analysis-friendly processors: a
comeback of model checking . . . . . . . 515--543
Vladimir Herdt and
Hoang M. Le and
Daniel Große and
Rolf Drechsler Combining sequentialization-based
verification of multi-threaded C
programs with symbolic Partial Order
Reduction . . . . . . . . . . . . . . . 545--565
Thomas Gibson-Robinson and
Gavin Lowe Symmetry reduction in CSP model checking 567--605
Maurice H. ter Beek and
Axel Legay Quantitative variability modelling and
analysis . . . . . . . . . . . . . . . . 607--612
Lars Luthmann and
Timo Gerecht and
Malte Lochau Sampling strategies for product lines
with unbounded parametric real-time
constraints . . . . . . . . . . . . . . 613--633
Maxime Cordy and
Axel Legay Verification and abstraction of
real-time variability-intensive systems 635--649
Linda Herrmann and
Martin Küttler and
Tobias Stumpf and
Christel Baier and
Hermann Härtig and
Sascha Klüppelholz Configuration of inter-process
communication with probabilistic model
checking . . . . . . . . . . . . . . . . 651--666
Uli Fahrenberg and
Axel Legay Quantitative properties of featured
automata . . . . . . . . . . . . . . . . 667--677
Davide Basile Applying supervisory control synthesis
to priced featured automata and energy
problems . . . . . . . . . . . . . . . . 679--689
Ferruccio Damiani and
Michael Lienhardt and
Luca Paolini Automatic refactoring of delta-oriented
SPLs to remove-free form and
replace-free form . . . . . . . . . . . 691--707
Alessandra Russo and
Andy Schürr Model-based software quality assurance
tools and techniques presented at FASE
2018 . . . . . . . . . . . . . . . . . . 1--2
Fotios Gioulekas and
Peter Poplavko and
Panagiotis Katsaros and
Saddek Bensalem and
Pedro Palomo Correct-by-construction model-based
design of reactive streaming software
for multi-core embedded systems . . . . 3--32
Fotios Gioulekas and
Peter Poplavko and
Panagiotis Katsaros and
Saddek Bensalem and
Pedro Palomo Correction to: Correct-by-construction
model-based design of reactive streaming
software for multi-core embedded systems 33--34
Aleksandar S. Dimovski CTL$^\star $ family-based model checking
using variability abstractions and modal
transition systems . . . . . . . . . . . 35--55
Oszkár Semeráth and
Rebeka Farkas and
Gábor Bergmann and
Dániel Varró Diversity of graph models and graph
generators in mutation testing . . . . . 57--78
Márton Búr and
Gábor Szilágyi and
András Vörös and
Dániel Varró Distributed graph queries over
models@run.time for runtime monitoring
of cyber-physical systems . . . . . . . 79--102
María del Mar Gallardo and
Pedro Merino Introduction to the Special Issue
devoted to SPIN 2018 . . . . . . . . . . 103--104
Laura Panizo and
Almudena Díaz and
Bruno García Model-based testing of apps in real
network scenarios . . . . . . . . . . . 105--114
Marek Chalupa and
Jan Strejcek and
Martina Vitovská Joint forces for memory safety checking
revisited . . . . . . . . . . . . . . . 115--133
Tim Lange and
Martin R. Neuhäußer and
Thomas Noll and
Joost-Pieter Katoen IC3 software model checking . . . . . . 135--161
Bernard Berthomieu and
Didier Le Botlan and
Silvano Dal Zilio Counting Petri net markings from
reduction equations . . . . . . . . . . 163--181
Hamzeh M. Allawi and
Waref Al Manaseer and
Mohammad Al Shraideh A greedy particle swarm optimization
(GPSO) algorithm for testing real-world
smart card applications . . . . . . . . 183--194
Fabrizio Banci Buonamici and
Gina Belmonte and
Vincenzo Ciancia and
Diego Latella and
Mieke Massink Spatial logics and model checking for
medical imaging . . . . . . . . . . . . 195--217
Hana Mkaouar and
Bechir Zalila and
Jérôme Hugues and
Mohamed Jmaiel A formal approach to AADL model-based
software engineering . . . . . . . . . . 219--247
Michael Butler and
Thai Son Hoang and
Alexander Raschke and
Klaus Reichl Introduction to special section on the
ABZ 2018 case study: Hybrid ERTMS/ETCS
Level 3 . . . . . . . . . . . . . . . . 249--255
Jean-Raymond Abrial The ABZ-2018 case study with Event-B . . 257--264
Paolo Arcaini and
Jan Kofron and
Pavel Jezek Validation of the Hybrid ERTMS/ETCS
Level 3 using Spin . . . . . . . . . . . 265--279
Alcino Cunha and
Nuno Macedo Validating the Hybrid ERTMS/ETCS Level 3
concept with Electrum . . . . . . . . . 281--296
Dana Dghaym and
Mohammadsadegh Dalvandi and
Michael Poppleton and
Colin Snook Formalising the Hybrid ERTMS Level 3
specification in iUML-B and Event-B . . 297--313
Dominik Hansen and
Michael Leuschel and
Philipp Körner and
Sebastian Krings and
Thomas Naulin and
Nader Nayeri and
David Schneider and
Frank Skowron Validation and real-life demonstration
of ETCS hybrid level 3 principles using
a formal B model . . . . . . . . . . . . 315--332
Amel Mammar and
Marc Frappier and
Steve Jeffrey Tueno Fotso and
Régine Laleau A formal refinement-based analysis of
the hybrid ERTMS/ETCS Level 3 standard 333--347
Steve Jeffrey Tueno Fotso and
Marc Frappier and
Régine Laleau and
Amel Mammar Modeling the hybrid ERTMS/ETCS Level 3
standard using a formal requirements
engineering approach . . . . . . . . . . 349--363
Ali Parsai and
Serge Demeyer Comparing mutation coverage against
branch coverage in an industrial setting 365--388
Rocco De Nicola and
Stefan Jähnichen and
Martin Wirsing Rigorous engineering of collective
adaptive systems: special section . . . 389--397
Dhaminda B. Abeywickrama and
Nicola Bicocchi and
Franco Zambonelli The SOTA approach to engineering
collective adaptive systems . . . . . . 399--415
Houssem Ben Mahfoudh and
Giovanna Di Marzo Serugendo and
Nabil Abdennadher Learning-based coordination model for
spontaneous self-composition of reliable
services in a distributed system . . . . 417--436
Rocco De Nicola and
Alessandro Maggi and
Joseph Sifakis The DReAM framework for dynamic
reconfigurable architecture modelling:
theory and applications . . . . . . . . 437--455
Thomas Gabor and
Andreas Sedlmeier and
Claudia Linnhoff-Popien The scenario coevolution paradigm:
adaptive quality assurance for adaptive
systems . . . . . . . . . . . . . . . . 457--476
Yehia Abd Alrahman and
Giulio Garbi A distributed API for coordinating AbC
programs . . . . . . . . . . . . . . . . 477--496
Tomas Bures and
Ilias Gerostathopoulos and
Jan Kofron A language and framework for dynamic
component ensembles in smart systems . . 497--509
Rima Al Ali and
Tomas Bures and
Jiri Vinarek Toward autonomically composable and
context-dependent access control
specification through ensembles . . . . 511--522
Milan Ceska and
Vojtech Havlena and
Tomás Vojnar Approximate reduction of finite automata
for high-speed network intrusion
detection . . . . . . . . . . . . . . . 523--539
Elvio G. Amparore and
Susanna Donatelli and
Gianfranco Ciardo Variable order metrics for decision
diagrams in system verification . . . . 541--562
Fabrizio Biondi and
Thomas Given-Wilson and
Axel Legay Introduction to the special issue for
SPIN 2019 . . . . . . . . . . . . . . . 563--564
Patrick Metzler and
Neeraj Suri and
Georg Weissenbacher Extracting safe thread schedules from
incomplete model checking results . . . 565--581
Richard DeFrancisco and
Shenghsun Cho and
Scott A. Smolka Swarm model checking on the GPU . . . . 583--599
Muhammad Usman and
Wenxi Wang and
Sarfraz Khurshid A study of learning likely data
structure properties using machine
learning models . . . . . . . . . . . . 601--615
Farnaz Yousefi and
Ehsan Khamespanah and
Ali Movaghar VeriVANca framework: verification of
VANETs by property-based message passing
of actors in Rebeca with inheritance . . 617--633
Sòren Enevoldsen and
Kim G. Larsen and
Jirí Srba Dependency graphs with applications to
verification . . . . . . . . . . . . . . 635--654
Yi Li and
Wenyuan Wu and
Yong Feng On ranking functions for single-path
linear-constraint loops . . . . . . . . 655--666
Luis Diogo Couto and
Peter W. V. Tran-Jòrgensen and
Peter Gorm Larsen Enabling continuous integration in a
formal methods setting . . . . . . . . . 667--683
Dirk Beyer and
Marieke Huisman Tools for the construction and analysis
of systems . . . . . . . . . . . . . . . 685--687
Iulia Dragomir and
Viorel Preoteasa and
Stavros Tripakis The Refinement Calculus of Reactive
Systems Toolset . . . . . . . . . . . . 689--708
Alexander J. Summers and
Peter Müller Automating deductive verification for
weak-memory programs (extended version) 709--728
Bernd Finkbeiner and
Christopher Hahn and
Leander Tentrup Efficient monitoring of hyperproperties
using prefix trees . . . . . . . . . . . 729--740
Dejan Nickovi\'c and
Olivier Lebeltel and
Dogan Ulus AMT 2.0: qualitative and quantitative
trace analysis with extended signal
temporal logic . . . . . . . . . . . . . 741--758
Carlos E. Budde and
Pedro R. D'Argenio and
Sean Sedwards An efficient statistical model checker
for nondeterminism and rare events . . . 759--780
Georgios Giantamidis and
Stavros Tripakis and
Stylianos Basagiannis Learning Moore machines from
input--output traces . . . . . . . . . . 1--29
Chris Alvin and
Brian Peterson and
Supratik Mukhopadhyay Static generation of UML sequence
diagrams . . . . . . . . . . . . . . . . 31--53
Yue Yuan and
Yi Li and
Wenchang Shi Detecting multiphase linear ranking
functions for single-path
linear-constraint loops . . . . . . . . 55--67
Florian Kammüller and
Axel Legay and
Stefano Schivo Masterminding change by combining secure
system design with security risk
assessment . . . . . . . . . . . . . . . 69--70
Pietro Ferrara and
Amit Kr Mandal and
Fausto Spoto Static analysis for discovering IoT
vulnerabilities . . . . . . . . . . . . 71--88
René Rydhof Hansen and
Kim Guldstrand Larsen and
Danny Bògsted Poulsen ADTLang: a programming language approach
to attack defense trees . . . . . . . . 89--104
Vladimir Shakhov and
Insoo Koo Graph-based technique for survivability
assessment and optimization of IoT
applications . . . . . . . . . . . . . . 105--114
Omar M. Alhawi and
Herbert Rocha and
Eddie Batista Verification and refutation of C
programs based on $k$-induction and
invariant inference . . . . . . . . . . 115--135
Raphaël Khoury and
Sylvain Hallé and
Yannick Lebrun Automata-based monitoring for LTL-FO$^+$ 137--154
Martin Leucker and
Christian Colombo Preface . . . . . . . . . . . . . . . . 155--156
Felipe Gorostiaga and
César Sánchez Stream runtime verification of real-time
event streams with the Striver language 157--183
Joshua Schneider and
David Basin and
Dmitriy Traytel Scalable online first-order monitoring 185--208
Giles Reger and
David Rydeheard From parametric trace slicing to rule
systems . . . . . . . . . . . . . . . . 209--228
Patricia Bouyer and
Léo Henry and
Nicolas Markey Diagnosing timed automata using timed
markings . . . . . . . . . . . . . . . . 229--253
Yli\`es Falcone and
Srdan Krsti\'c and
Dmitriy Traytel A taxonomy for classifying runtime
verification tools . . . . . . . . . . . 255--284
Reiner Hähnle and
Wil van der Aalst Automated model analysis tools and
techniques presented at FASE 2019 . . . 285--287
Artur Boronat Incremental execution of rule-based
model transformation . . . . . . . . . . 289--311
Dirk Beyer and
Marie-Christine Jakobs Cooperative verifier-based testing with
CoVeriTest . . . . . . . . . . . . . . . 313--333
Lars Fritsche and
Jens Kosiol and
Gabriele Taentzer Avoiding unnecessary information loss:
correct and efficient model
synchronization based on triple graph
grammars . . . . . . . . . . . . . . . . 335--368
Sven Schneider and
Leen Lambers and
Fernando Orejas A logic-based incremental approach to
graph repair featuring delta
preservation . . . . . . . . . . . . . . 369--410
Sven Schneider and
Maria Maximova and
Holger Giese Formal testing of timed graph
transformation systems using metric
temporal graph logic . . . . . . . . . . 411--488
Paul Dubrulle and
Nikolai Kosmatov and
Arnault Lapitre \pkgPolyGraph: a data flow model with
frequency arithmetic . . . . . . . . . . 489--517
Paul Dubrulle and
Nikolai Kosmatov and
Arnault Lapitre Correction to: \pkgPolyGraph: a data
flow model with frequency arithmetic . . 519--519
Markus Frohme and
Bernhard Steffen Compositional learning of mutually
recursive procedural systems . . . . . . 521--543
Bernd Finkbeiner and
Leonardo Mariani Introduction to the special issue of the
19th International Conference on Runtime
Verification . . . . . . . . . . . . . . 545--546
Klaus Havelund and
Doron Peled An extension of first-order LTL with
rules with application to runtime
verification . . . . . . . . . . . . . . 547--563
Dejan Nickovi\'c and
Xin Qin and
Jyotirmoy Deshmukh Specifying and detecting temporal
patterns with shape expressions . . . . 565--577
Sean Kauffman and
Klaus Havelund and
Sebastian Fischmeister What can we monitor over unreliable
channels? . . . . . . . . . . . . . . . 579--600
Luca Aceto and
Ian Cassar and
Anna Ingólfsdóttir Comparing controlled system synthesis
and suppression enforcement . . . . . . 601--614
Luca Bortolussi and
Francesca Cairoli and
Scott D. Stoller Neural predictive monitoring and a
comparison of frequentist and Bayesian
approaches . . . . . . . . . . . . . . . 615--640
Saeid Tizpaz-Niari and
Pavol Cerný and
Ashutosh Trivedi Quantitative estimation of side-channel
leaks with neural networks . . . . . . . 641--654
Dawid Kopetzki and
Michael Lybecait and
Bernhard Steffen Towards language-to-language
transformation . . . . . . . . . . . . . 655--677
Simon Bliudze and
Panagiotis Katsaros and
Martin Wirsing On methods and tools for rigorous system
design . . . . . . . . . . . . . . . . . 679--684
Christos Grompanopoulos and
Antonios Gouglidis and
Anastasia Mavridou Specifying and verifying usage control
models and policies in TLA$^+$ . . . . . 685--700
Rim El Ballouli and
Saddek Bensalem and
Joseph Sifakis Programming dynamic reconfigurable
systems . . . . . . . . . . . . . . . . 701--719
Pujie Han and
Zhengjun Zhai and
Ulrik Nyman Model-based optimization of ARINC-653
partition scheduling . . . . . . . . . . 721--740
S. Blom and
S. Darabi and
M. Safari Correct program parallelisations . . . . 741--763
Alexios Lekidis and
Panagiotis Katsaros Energy characterization of IoT systems
through design aspect monitoring . . . . 765--781
Ezio Bartocci and
Niveditha Manjunath and
Dejan Nickovi\'c CPSDebug: Automatic failure explanation
in CPS models . . . . . . . . . . . . . 783--796
Nathalie Bertrand and
Igor Konnov and
Josef Widder Verification of randomized consensus
algorithms under round-rigid adversaries 797--821
Nathalie Bertrand and
Igor Konnov and
Josef Widder Correction to: Verification of
randomized consensus algorithms under
round-rigid adversaries . . . . . . . . 823--823
Parosh Aziz Abdulla and
Frédéric Haziza and
Ahmed Rezine Correction to: An integrated
specification and verification technique
for highly concurrent data structures 825--825
Jan-David Quesel and
Stefan Mitsch and
André Platzer Correction to: How to model and prove
hybrid systems with \pkgKeYmaera: a
tutorial on safety . . . . . . . . . . . 827--827
Dirk Beyer and
Marieke Huisman TOOLympics I: Competition on software
testing . . . . . . . . . . . . . . . . 829--832
Dirk Beyer First international competition on
software testing . . . . . . . . . . . . 833--846
Marie-Christine Jakobs \pkgCoVeriTest: interleaving value and
predicate analysis for test-case
generation . . . . . . . . . . . . . . . 847--851
Sebastian Ruland and
Malte Lochau and
Andy Schürr \pkgCPA/Tiger-MGP: test-goal set
partitioning for efficient multi-goal
test-suite generation . . . . . . . . . 853--856
Mikhail R. Gadelha and
Rafael S. Menezes and
Lucas C. Cordeiro \pkgESBMC 6.1: automated test case
generation using bounded model checking 857--861
Caroline Lemieux and
Koushik Sen \pkgFairFuzz-TC: a fuzzer targeting rare
branches . . . . . . . . . . . . . . . . 863--866
Cristian Cadar and
Martin Nowack \pkgKLEE symbolic execution engine in
2019 . . . . . . . . . . . . . . . . . . 867--870
Thomas Lemberger Plain random test generation with
\pkgPRTest . . . . . . . . . . . . . . . 871--873
Marek Chalupa and
Martina Vitovská and
Jan Strejcek \pkgSymbiotic 6: generating test cases
by slicing and symbolic execution . . . 875--877
Dirk Beyer and
Marieke Huisman and
Bernhard Steffen TOOLympics II: competitions on formal
methods . . . . . . . . . . . . . . . . 879--881
Claire Dross and
Carlo A. Furia and
Peter Müller VerifyThis 2019: a program verification
competition . . . . . . . . . . . . . . 883--893
Mihaela Sighireanu SL-COMP: competition of solvers for
separation logic . . . . . . . . . . . . 895--903
Aart Middeldorp and
Julian Nagele and
Kiraku Shintani CoCo 2019: report on the eighth
confluence competition . . . . . . . . . 905--916
Falk Howar and
Marc Jasper and
Bernhard Steffen The RERS challenge: towards controllable
and scalable benchmark synthesis . . . . 917--930
Fabrice Kordon and
Lom Messan Hillah and
Emmanuel Paviot-Adet Study of the efficiency of model
checking techniques using results of the
MCC from 2015 To 2019 . . . . . . . . . 931--952
Lukás Charvát and
Ales Smrcka and
Tomás Vojnar Utilizing parametric systems for
detection of pipeline hazards . . . . . 1--28
Tomás Vojnar and
Lijun Zhang Tools and algorithms for the
construction and analysis of systems: a
special issue for TACAS 2019 . . . . . . 29--31
Ilina Stoilkovska and
Igor Konnov and
Florian Zuleger Verifying safety of synchronous
fault-tolerant algorithms by bounded
model checking . . . . . . . . . . . . . 33--48
Sòren Enevoldsen and
Kim Guldstrand Larsen and
Jirí Srba Extended abstract dependency graphs . . 49--65
Petar Vukmirovi\'c and
Jasmin Blanchette and
Stephan Schulz Extending a brainiac prover to
lambda-free higher-order logic . . . . . 67--87
Junaid Babar and
Gianfranco Ciardo and
Andrew Miner CESRBDDs: binary decision diagrams with
complemented edges and edge-specified
reductions . . . . . . . . . . . . . . . 89--109
Martin Blicha and
Antti E. J. Hyvärinen and
Natasha Sharygina Using linear algebra in decomposition of
Farkas interpolants . . . . . . . . . . 111--125
Alexandre Vernotte and
Aymeric Cretin and
Fabien Peureux A domain-specific language to design
false data injection tests for air
traffic control systems . . . . . . . . 127--158
Antoine El-Hokayem and
Yli\`es Falcone Bringing runtime verification home: a
case study on the hierarchical
monitoring of smart homes using
decentralized specifications . . . . . . 159--181
Marlon Dumas and
Luciano García-Bañuelos and
Maksym Yerokhin Multi-level privacy analysis of business
processes: the Pleak toolset . . . . . . 183--203
Paul-Antoine Arras and
Anastasios Andronidis and
Cristian Cadar SaBRe: load-time selective binary
rewriting . . . . . . . . . . . . . . . 205--223
Hassna Louadah and
Yvan Labiche Interface control document modeling with
Citrus (avionics systems interfaces) . . 225--245
Lorenzo Bettini and
Davide Di Ruscio and
Alfonso Pierantonio Supporting safe metamodel evolution with
edelta . . . . . . . . . . . . . . . . . 247--260
Per Erik Strandberg and
Wasif Afzal and
Daniel Sundmark Software test results exploration and
visualization with continuous
integration and nightly testing . . . . 261--285
Gavin Lowe Parameterized verification of systems
with component identities, using view
abstraction . . . . . . . . . . . . . . 287--324
Maurice H. ter Beek and
Kim G. Larsen and
Tim A. C. Willemse Formal methods and tools for industrial
critical systems . . . . . . . . . . . . 325--330
Norman Weik and
Matthias Volk and
Nils Nießen DFT modeling approach for operational
risk assessment of railway
infrastructure . . . . . . . . . . . . . 331--350
Davide Basile and
Maurice H. ter Beek and
Axel Legay Exploring the ERTMS/ETCS full moving
block specification: an experience with
formal methods . . . . . . . . . . . . . 351--370
Yanni Kouskoulas and
T. J. Machado and
Joshua Brulé Envelopes and waves: safe multivehicle
collision avoidance for horizontal
non-deterministic turns . . . . . . . . 371--394
Rong Gu and
Peter G. Jensen and
Kristina Lundqvist Verifiable strategy synthesis for
multiple autonomous agents: a scalable
approach . . . . . . . . . . . . . . . . 395--414
Benjamin Binder and
Mihail Asavoae and
Mathieu Jan Formal modeling and verification for
amplification timing anomalies in the
superscalar TriCore architecture . . . . 415--440
Olav Bunte and
Louis C. M. van Gool and
Tim A. C. Willemse Formal verification of OIL component
specifications using mCRL2 . . . . . . . 441--472
Samuel Huang and
Rance Cleaveland Temporal-logic query checking over
finite data streams . . . . . . . . . . 473--492
Petr Rockai and
Jirí Barnat DivSIM, an interactive simulator for
LLVM bitcode . . . . . . . . . . . . . . 493--510
Elahe Habibi and
Seyed-Hasan Mirian-Hosseinabadi Generating test as a web service (TaaWS)
through a method-based attribute grammar 511--527
Sebastien Salva and
Elliott Blot Learning of behavioural models and
dependency graphs for communicating
systems with CkTailv2 . . . . . . . . . 529--548
H. M. W. Verbeek The Log Skeleton Visualizer in ProM 6.9 549--561
Christoffer Olling Back and
Tijs Slaats and
Thomas Troels Hildebrandt and
Morten Marquard DisCoveR: accurate and efficient
discovery of declarative process models 563--587
Christian Hensel and
Sebastian Junges and
Joost-Pieter Katoen and
Tim Quatmann and
Matthias Volk The probabilistic model checker Storm 589--610
Axel Legay and
Tiziana Margaria Tools and algorithms for the
construction and analysis of systems: a
special issue for TACAS 2017 . . . . . . 611--612
Pedro Antonino and
Thomas Gibson-Robinson and
A. W. Roscoe Approximate verification of concurrent
systems using token structures and
invariants . . . . . . . . . . . . . . . 613--633
Javier Esparza and
Jan K\vret\'ìnský and
Jean-François Raskin and
Salomon Sickert From linear temporal logic and
limit-deterministic Büchi automata to
deterministic parity automata . . . . . 635--659
Dirk Beyer and
Stefan Löwe and
Philipp Wendler Correction to: Reliable benchmarking:
requirements and solutions . . . . . . . 661--661
Armin Biere and
David Parker Tools and algorithms for the
construction and analysis of systems: a
special issue for TACAS 2020 . . . . . . 663--665
Hadar Frenkel and
Orna Grumberg and
Corina S. P\uas\uareanu and
Sarai Sheinvald Assume, guarantee or repair: a regular
framework for non regular properties . . 667--689
Florian Frohn and
Carsten Fuhs A calculus for modular loop acceleration
and non-termination proofs . . . . . . . 691--715
Benedikt Becker and
Nicolas Jeannerod and
Claude Marché and
Yann Régis-Gianas and
Mihaela Sighireanu and
Ralf Treinen The CoLiS platform for the analysis of
maintainer scripts in Debian software
packages . . . . . . . . . . . . . . . . 717--733
Thomas Neele and
Tim A. C. Willemse and
Wieger Wesselink and
Antti Valmari Partial-order reduction for parity games
and parameterised Boolean equation
systems . . . . . . . . . . . . . . . . 735--756
Ruben Hamers and
Erik Horlings and
Sung-Shik Jongmans The Discourje project: run-time
verification of communication protocols
in Clojure . . . . . . . . . . . . . . . 757--782
Hans-Dieter A. Hiep and
Olaf Maathuis and
Jinting Bian and
Frank S. de Boer and
Stijn de Gouw Verifying OpenJDK's LinkedList using KeY
(extended paper) . . . . . . . . . . . . 783--802
Thom Badings and
Murat Cubuktepe and
Nils Jansen and
Sebastian Junges and
Joost-Pieter Katoen and
Ufuk Topcu Scenario-based verification of uncertain
parametric MDPs . . . . . . . . . . . . 803--819
Carlos E. Budde and
Pedro R. D'Argenio and
Raúl E. Monti and
Mariëlle Stoelinga Analysis of non-Markovian repairable
fault trees through rare event
simulation . . . . . . . . . . . . . . . 821--841
Supratik Chakraborty and
Ashutosh Gupta and
Divyesh Unadkat Full-program induction: verifying array
programs sans loop invariants . . . . . 843--888
Mawal A. Mohammed and
Jameleddine Hassine and
Mohammad Alshayeb GSDetector: a tool for automatic
detection of bad smells in GRL goal
models . . . . . . . . . . . . . . . . . 889--910
Jaehun Lee and
Kyungmin Bae and
Peter Csaba Ölveczky and
Sharon Kim and
Minseok Kang Modeling and formal analysis of
virtually synchronous cyber-physical
systems in AADL . . . . . . . . . . . . 911--948
Ramsay G. Taylor and
Michael Foster and
Siobhán North An automated framework for verifying or
refuting trace properties of extended
finite state machines . . . . . . . . . 949--972
Alberto Lluch Lafuente and
Anastasia Mavridou Formal methods and tools for industrial
critical systems . . . . . . . . . . . . 973--976
Cláudio Belo Lourenço and
Denis Cousineau and
Florian Faissole and
Claude Marché and
David Mentré and
Hiroaki Inoue Automated formal analysis of temporal
properties of Ladder programs . . . . . 977--997
Simon Thrane Hansen and
Casper Thule and
Cláudio Gomes and
Jaco van de Pol and
Maurizio Palmieri and
Emin Oguz Inci and
Frederik Madsen and
Jesús Alfonso and
José Ángel Castellanos and
José Manuel Rodriguez Verification and synthesis of
co-simulation algorithms subject to
algebraic loops and adaptive steps . . . 999--1024
Andrej Kiviriga and
Kim Guldstrand Larsen and
Ulrik Nyman Randomized reachability analysis in
UPPAAL: fast error detection in timed
systems . . . . . . . . . . . . . . . . 1025--1042
Joshua Schmidt and
Michael Leuschel SMT solving for the validation of B and
Event-B models . . . . . . . . . . . . . 1043--1077
Alessandro Berti and
Wil M. P. van der Aalst OC-PM: analyzing object-centric event
logs and process models . . . . . . . . 1--17
Sascha Lehmann and
Sibylle Schupp Bounded DBM-based clock state
construction for timed automata in
Uppaal . . . . . . . . . . . . . . . . . 19--47
Martina De Sanctis and
Amleto Di Salle and
Ludovico Iovino and
Maria Teresa Rossi A technology transfer journey to a
model-driven access control system . . . 49--74
Alfons Laarman and
Ana Sokolova Introduction to the special issue for
SPIN 2021 . . . . . . . . . . . . . . . 75--76
Alexandre Kirszenberg and
Antoine Martin and
Hugo Moreau and
Etienne Renault Go2Pins: a framework for the LTL
verification of Go programs (extended
version) . . . . . . . . . . . . . . . . 77--94
Nicolas Amat and
Silvano Dal Zilio and
Didier Le Botlan Leveraging polyhedral reductions for
solving Petri net reachability problems 95--114
Madoda Nxumalo and
Nils Timm and
Stefan Gruner An evaluation of approaches to model
checking real-time task schedulability
analysis . . . . . . . . . . . . . . . . 115--128
Peter Gjòl Jensen and
Thomas Neele Tools and algorithms for the
construction and analysis of systems: a
special issue on tool papers for TACAS
2021 . . . . . . . . . . . . . . . . . . 129--131
Daniela Kaufmann and
Armin Biere Improving AMulet2 for verifying
multiplier circuits using SAT solving
and computer algebra . . . . . . . . . . 133--144
Matthew Sotoudeh and
Zhe Tao and
Aditya V. Thakur SyReNN: a tool for analyzing deep neural
networks . . . . . . . . . . . . . . . . 145--165
Yong Kiam Tan and
Marijn J. H. Heule and
Magnus O. Myreen Verified Propagation Redundancy and
Compositional UNSAT Checking in CakeML 167--184
Rosa Abbasi and
Jonas Schiffl and
Eva Darulova and
Mattias Ulbrich and
Wolfgang Ahrendt Combining rule- and SMT-based reasoning
for verifying floating-point Java
programs in KeY . . . . . . . . . . . . 185--204
Sebastian Biewer and
Bernd Finkbeiner and
Holger Hermanns and
Maximilian A. Köhl and
Yannik Schnitzer and
Maximilian Schwenger On the road with RTLola . . . . . . . . 205--218
Joseph Scott and
Aina Niemetz and
Mathias Preiner and
Saeed Nejati and
Vijay Ganesh Algorithm selection for SMT . . . . . . 219--239
Nils Jansen and
Gerrit Nolte and
Bernhard Steffen Explanation Paradigms Leveraging
Analytic Intuition (ExPLAIn) . . . . . . 241--247
Florian Jüngermann and
Jan Kretínský and
Maximilian Weininger Algebraically explainable controllers:
decision trees and support vector
machines join forces . . . . . . . . . . 249--266
Frederik Gossen and
Bernhard Steffen Algebraic aggregation of random forests:
towards explainability and rapid
evaluation . . . . . . . . . . . . . . . 267--285
Alnis Murtovi and
Alexander Bainczyk and
Gerrit Nolte and
Maximilian Schlüter and
Bernhard Steffen Forest GUMP: a tool for verification and
explanation . . . . . . . . . . . . . . 287--299
Maximilian Schlüter and
Gerrit Nolte and
Alnis Murtovi and
Bernhard Steffen Towards rigorous understanding of neural
networks via semantics-preserving
transformations . . . . . . . . . . . . 301--327
Christopher Brix and
Mark Niklas Müller and
Stanley Bak and
Taylor T. Johnson and
Changliu Liu First three years of the international
verification of neural networks
competition (VNN-COMP) . . . . . . . . . 329--339
Igor Khmelnitsky and
Daniel Neider and
Rajarshi Roy and
Xuan Xie and
Beno\^\it Barbot and
Benedikt Bollig and
Alain Finkel and
Serge Haddad and
Martin Leucker and
Lina Ye Analysis of recurrent neural networks
via property-directed verification of
surrogate models . . . . . . . . . . . . 341--354
Gerrit Nolte and
Maximilian Schlüter and
Alnis Murtovi and
Bernhard Steffen The power of typed affine decision
structures: a case study . . . . . . . . 355--374
Thom Badings and
Thiago D. Simão and
Marnix Suilen and
Nils Jansen Decision-making under uncertainty:
beyond probabilities . . . . . . . . . . 375--391
Muhammad Usman and
Youcheng Sun and
Divya Gopinath and
Rishi Dange and
Luca Manolache and
Corina S. P\uas\uareanu An overview of structural coverage
metrics for testing neural networks . . 393--405
Timo P. Gros and
Holger Hermanns and
Jörg Hoffmann and
Michaela Klauck and
Marcel Steinmetz Analyzing neural network behavior
through deep statistical model checking 407--426
Jyotirmoy Deshmukh and
Dejan Nickovi\'c Introduction to the Special Issue on
Runtime Verification . . . . . . . . . . 427--429
Vivian M. Ho and
Chris Alvin and
Jimmie D. Lawson and
Supratik Mukhopadhyay and
Brian Peterson Program analysis using empirical
abstraction . . . . . . . . . . . . . . 431--452
Chukri Soueidi and
Marius Monnier and
Yli\`es Falcone Efficient and expressive bytecode-level
instrumentation for Java programs . . . 453--479
Nastaran Shafiei and
Klaus Havelund and
Peter Mehlitz Concurrent runtime verification of data
rich events . . . . . . . . . . . . . . 481--501
Laura Nenzi and
Ezio Bartocci and
Luca Bortolussi and
Simone Silvetti and
Michele Loreti MoonLight: a lightweight tool for
monitoring spatio-temporal properties 503--517
Lu Feng and
Dana Fisman Introduction to the Special Issue on
Runtime Verification . . . . . . . . . . 519--520
Vimuth Fernando and
Keyur Joshi and
Jacob Laurel and
Sasa Misailovic Diamont: dynamic monitoring of
uncertainty for distributed asynchronous
programs . . . . . . . . . . . . . . . . 521--539
Anik Momtaz and
Niraj Basnet and
Houssam Abbas and
Borzoo Bonakdarpour Predicate monitoring in distributed
cyber-physical systems . . . . . . . . . 541--556
Konstantinos Mamouras and
Agnishom Chattopadhyay and
Zhifu Wang A compositional framework for algebraic
quantitative online monitoring over
continuous-time signals . . . . . . . . 557--573
Konstantin Kueffner and
Anna Lukina and
Christian Schilling and
Thomas A. Henzinger Into the unknown: active monitoring of
neural networks (extended version) . . . 575--592
Jan Baumeister and
Johann C. Dauer and
Bernd Finkbeiner and
Sebastian Schirmer Monitoring with verified guarantees . . 593--616
Martin Wirsing and
Stefan Jähnichen and
Rocco De Nicola Rigorous engineering of collective
adaptive systems --- 2nd special section 617--624
Marius Bozga and
Joseph Sifakis Correct by design coordination of
autonomous driving systems . . . . . . . 625--639
Davide Basile and
Maurice H. ter Beek and
Laura Bussi and
Vincenzo Ciancia A toolchain for strategy synthesis with
spatial properties . . . . . . . . . . . 641--658
Peter Fettke and
Wolfgang Reisig A causal, time-independent
synchronization pattern for collective
adaptive systems . . . . . . . . . . . . 659--673
Rocco De Nicola and
Luca Di Stefano and
Omar Inverso and
Serenella Valiani Modelling flocks of birds and colonies
of ants from the bottom up . . . . . . . 675--691
Stefania Monica and
Federico Bergenti and
Franco Zambonelli A kinetic approach to investigate the
collective dynamics of multi-agent
systems . . . . . . . . . . . . . . . . 693--705
Chen Yifeng and
J. W. Sanders A modal approach to conscious social
agents . . . . . . . . . . . . . . . . . 707--716
Michal Töpfer and
Milad Abdullah and
Tomá\vs Bure\vs and
Petr Hn\vetynka and
Martin Kruli\vs Machine-learning abstractions for
component-based self-optimizing systems 717--731
Tomá\vs Bure\vs and
Petr Hn\vetynka and
Martin Kruli\vs and
Franti\vsek Plá\vsil and
Danylo Khalyeyev and
Sebastian Hahner and
Stephan Seifermann and
Maximilian Walter and
Robert Heinrich Generating adaptation rule-specific
neural networks . . . . . . . . . . . . 733--746
Lorenzo Bettini and
Khalid Bourr and
Rosario Pugliese and
Francesco Tiezzi Coordinating and programming multiple
ROS-based robots with X-KLAIM . . . . . 747--764
Yehia Abd Alrahman and
Shaun Azzopardi and
Luca Di Stefano and
Nir Piterman Language support for verifying
reconfigurable interacting systems . . . 765--784
Maurizio Murgia and
Riccardo Pinciroli and
Catia Trubiani and
Emilio Tuosto Comparing performance abstractions for
collective adaptive systems . . . . . . 785--798
Joseph Scott and
Aina Niemetz and
Mathias Preiner and
Saeed Nejati and
Vijay Ganesh Publisher Correction: Algorithm
selection for SMT . . . . . . . . . . . 799--800