Preface

The aim of GRAPHITE is to foster the convergence on research interests from several communities dealing with graph analysis in all its forms in computer science, with a particular attention to software development and analysis. Graphs are used to represent data and processes in many application areas, and they are subjected to various computational algorithms in order to analyze them. Just restricting the attention to the analysis of software, graph analysis algorithms are used, for instance, to verify properties using model checking techniques that explore the system's state space graph or static analysis techniques based on control flow graphs. Further application domains include games, planning, and network analysis. Very often, graph problems and their algorithmic solutions have common characteristics, independent of their application domain. The goal of this event is to gather scientists from different communities, who do research on graph analysis algorithms, such that awareness of each others' work is increased.

The first two workshops were held as satellite events of ETAPS 2012 and 2013. In 2009, the same motivation led to organising Dagstuhl Seminar 09491, entitled "Graph Search Engineering". The GRAPHITE workshop resulted from the overall success of that seminar.

This year, Radu Mateescu from the CONVECS team at INRIA Grenoble - Rhône-Alpes was our invited speaker. His talk was titled Walking Back and Forth in Labelled Transition Systems.

Besides that, we also had a call for technical papers. Each contribution went through a thorough reviewing process. For this, we would like to thank the GRAPHITE 2014 program committee members:

• Klemens Böhm (Karlsruhe Institute of Technology, Germany)
• Pierluigi Crescenzi (University of Florence, Italy)
• Keijo Heljanko (Aalto University, Finland)
• Martin Hofmann (LMU Munich, Germany)
• Jeroen Ketema (Imperial College London, UK)
• Barbara König (University of Duisburg-Essen, Germany)
• Stefan Leue (University of Konstanz, Germany)
• David Lo (Singapore Management University, Singapore)
• Michele Loreti (University of Florence, Italy)
• Mila Majster-Cederbaum (LMU Munich, Germany)
• Mieke Massink (CNR-ISTI Pisa, Italy)
• Dave Parker (University of Birmingham, UK)
• Arend Rensink (University of Twente, The Netherlands)
• Andrey Rybalchenko (Microsoft Research Cambridge, UK and TU Munich, Germany)
• Gwen Salaün (Grenoble INP, Inria, France)
• Valerio Senni (IMT Institute of Advanced Studies Lucca, Italy)
• Sebastiano Vigna (University of Milan, Italy)
• Willem Visser (University of Stellenbosch, South Africa)

We thank all the authors of submitted papers for their contributions, and all accepted papers for the quick turnaround in producing the camera-ready copies included in this proceedings. Finally, we thank the editorial board of EPTCS, and the workshops chair of ETAPS 2014, Axel Legay, for their support.

Dragan Bošnački
Stefan Edelkamp
Alberto Lluch Lafuente
Anton Wijs

Walking Back and Forth in Labelled Transition Systems

Graph exploration underlies several analysis problems defined on Labeled Transition Systems (LTSs), such as model checking, equivalence checking, tau-confluence reduction, pruning of undesirable behavior, etc. This talk gives an overview of the graph exploration techniques available in the CADP verification toolbox, their instantiation in verification tools (in particular, the Evaluator 4.0 and XTL model checkers), and their applications to the analysis of LTSs.