With the raise of Model-Driven Engineering (Mde), model transformations are more and more used as the automation technique in software engineering. After more than a decade of maturation, Mde can nowadays leverage software development within complex domains and for building large-scale systems, thanks to the recent theoretical foundations and emerging tool support. In this respect, the correctness of model transformations is one crucial requirement for the success of Mde. Despite some recent advances in this eld, the work on the Veri cation & Validation (V&V) of model transformations still remains scattered, and a clear perspective on the subject is still an ongoing process. The International Workshop on Veri cation of Model Transformations (Volt) is one of the most accurate venues to o er researchers a dedicated forum to classify, discuss, propose, and advance veri cation techniques dedicated to model transformations. This fourth edition has been held as a full-day event of the Staf (Software Technologies: Applications and Foundations) federation of conferences on the July 23rd, 2015 in L'Aquila, Italy. In this edition of VOLT, we strongly encouraged the authors to tackle in their submissions three transformation veri cation challenges concerning: (i) a purely structural translation consisting of the classical UML2RDMS transformation, (ii) an operational semantics of a Domain-Speci c Language allowing to play to the well-known PacMan game, and (iii) a translational semantics providing executability of (a signi cant portion of) Activity Diagrams in terms of Petri Nets. The metamodels, models, and transformations as well as the properties to be speci ed and veri ed have been provided by the organizers. Five contributions were accepted after a rigorous review process, addressing these challenges by using di erent property languages as well as veri cation technology such as OCL, Boogie, NuSMV, and Flora-2. The workshop's program consisted of the accepted papers presentation, a keynote by Gabriele Taentzer on \Analysis Techniques for Graph Transformation Systems", and keynotes shared with the hosting conference federation. We would like to thank the STAF 2015 organization for giving us the opportunity to organize this workshop, especially to the general chair of STAF 2015 Alfonso Pierantonio (Universita degli Studi dell'Aquila, Italy) and to the workshops chairs Davide Di Ruscio (Universita degli Studi dell'Aquila, Italy) and Pieter Van Gorp (Eindhoven University of Technology, The Netherlands), who were always very helpful and supportive. Many thanks to all those that submitted papers, and particularly to the presenters of the accepted papers. We also warmly thank Gabriele Taentzer for providing a very inspiring keynote talk and the many participants who contributed to the open discussions with their comments and experience. Last but not least, our thanks go to the reviewers and the members of the Program Committee, for their timely and accurate reviews and for their help in choosing and suggestions for improving the selected papers.
Program Committee Mark Asztalos Dider Buchs Jordi Cabot Marsha Chechik Antonio Cichetti Juan De Lara Michalis Famelis Holger Giese Martin Gogolla Je Gray Esther Guerra Reiko Heckel Frank Hermann Akos Horvath Akram Idani Marouane Kessentini Dimitrios S. Kolovos Leen Lambers Kevin Lano Tihamer Levendovszky Levi Lucio Arend Rensink Rick Saley Martina Seidl Gabriele Taentzer Javier Troya Antonio Vallecillo Hans Vanghelhuwe