VOLT 2015 Co-located with STAF 2015 4th Workshop on the Verification of Model Transformation http://volt2015.big.tuwien.ac.at/ L'Aquila, Italy July 23, 2015 *** Call for Papers *** Model transformations are everywhere in software development. They have been described as the “heart and soul of Model-Driven Development (MDD)”. It is generally accepted that MDD is a very promising means for raising the level of abstraction of current software development techniques, while making it more reliable, efficient, safe and cost-effective. Several experts have identified the verification of model transformations as one of the grand challenges of the domain. Despite some recent activity in the field, the work on the verification of model transformations remains scattered and a clear perspective on the subject is still not in sight. Furthermore, current model transformation tools lack verification techniques to support such activities. If we generically consider a model transformation as an algorithm describing specific model manipulations, then testing it or proving some of its properties can be envisaged. However, a model transformation performs particular computations where: (1) it typically operates on models, thus on data at a high-level of abstraction rich in semantics and (2) from a pragmatic point of view, often only the initial input and the final output is of interest and none of the intermediate steps matters. Moreover, a particular subject of interest is the fact that model transformations are used to perform specific computations in the context of MDD, such as model refinement, refactoring, translation, synthesis, simulation, or synchronization. In this sense, we feel that useful verification techniques for model transformations can and possibly should be specific to these activities. The Fourth International Workshop on the Verification Of modeL Transformation (VOLT 2015) is one of the most accurate venues to offer researchers a dedicated forum to classify, discuss, propose, and advance verification techniques dedicated to model transformations. VOLT 2015 promotes discussions between theoreticians and practitioners from academy and industry, given its ideal co-location with STAF and in particular ECMFA, ICGT, ICMT, TTC, and TAP. VOLT’s interest spans both to academic and industrial practices. One of the goals of the forum is to collect enough industrial case studies so that those problems can be stated at a theoretical level. In order to discuss these and further similar questions, we would like to invite submissions in the form of regular papers, short papers (ongoing work, position statements), and demonstration papers (about novel tool features) related to the following topics: - Application of formal verification (e.g., theorem proving, model-checking or abstract interpretations) to model transformations: * Verification of model transformations expressed in languages such as ATL, QVT, TGG, Viatra, Kermeta, Epsilon, etc.; * Verification of Domain-Specific Model Transformations, in contrast to general-purpose transformations; * Verification techniques dedicated to model transformation; - Taxonomies of techniques for model transformation verification: * Properties relevant to techniques for model transformation verification; * Reviews and surveys on the practice of verification for model transformations; - Comparisons between formal verification techniques for model transformation versus general-purpose programming languages; - Case studies, comparisons, and experience reports; - Tools and automation. As a special issue this year, we also strongly encourage solutions to the following model transformation verification challenges: - a purely structural translation (aka. structural bridge) consisting of the classical UML2RDMS transformation; - an operational semantics of a Domain-Specific Language allowing to play to the well-known PacMan game; - a translational semantics providing executability of (a significant portion of) Activity Diagrams in terms of Petri Nets. All cases are well-documented transformations, so that contestants can focus on the verification tasks rather than the (correct) transformation design. More details about the transformations, as well as the associated requirements, are provided on the Workshop's webpage. *** Submission *** To comply with STAF's special theme of "reproducibility", submitted papers should fall down in one of these paper category, depending on the nature of the contribution: - Regular papers (up to 10 pages) which presents novel innovative approaches, should integrate our case studies either as a running example, or as a minimal case study for validation; - Short papers (up to 8 pages) which presents new ideas or ongoing research, are submitted to the same requirements as regular papers. - Tool/Demo papers (up to 6 pages) which should demonstrate our case studies by formally analysing their associated properties within a specific tool. All submissions should follow the Springer LNCS format and be submitted through the EasyChair installation: https://easychair.org/conferences/?conf=volt2015 A pre-workshop version of the papers will be available on the workshop website and a post-workshop version will be published as CEUR workshop proceedings (http://ceur-ws.org). We are aiming at a joint article comprising all solutions for the Case Studies. *** Workshop Format *** VOLT 2015 is a one-day workshop, divided into two parts: keynote, paper presentations, and tool demonstrations (morning) and discussions in working groups (afternoon). *** Important Dates *** Submission: May 22, 2015 Author notification: June 12, 2015 Final version: July 8, 2015 Workshop: July 23, 2015 *** Organization Committee *** Moussa AMRANI, University of Namur, Belgium Eugene SYRIANI, University of Montréal, Canada Manuel WIMMER, Vienna University of Technology, Austria *** Program Committee *** Mark Asztalos (Budapest University of Technology and Economics, Hungary) Dider Buchs (University of Geneva, Switzerland) Jordi Cabot (INRIA, France) Marsha Chechik (University of Toronto, Canada) Antonio Cichetti (Malardalen University in Vasteras, Sweden) Juan de Lara (Universidad Autónoma de Madrid, Spain) Michalis Famelis (University of Toronto, Canada) Holger Giese (Hasso-Plattner-Institute, Germany) Martin Gogolla (University of Bremen, Germany) Jeff Gray (University of Alabama, USA) Esther Guerra (Universidad Autónoma de Madrid, Spain) Reiko Heckel (University of Leicester, UK) Ákos Horváth (Budapest University of Technology and Economics, Hungary) Akram Idani (Grenoble INP, France) Marouane Kessentini (University of Michigan, USA) Leen Lambers (Hasso-Plattner-Institute, Germany) Kevin Lano (King's College London, UK) Tihamer Levendovszky (Vanderbilt University School of Engineering, USA) Levi Lucio (McGill University, Canada) Arend Rensink (University of Twente, Netherlands) Rick Saley (University of Toronto, Canada) Martina Seidl (University of Linz, Austria) Gabriele Taentzer (Philipps-Universität Marburg, Germany) Javier Troya (Vienna University of Technology, Austria) Antonio Vallecillo (Universidad de Málaga)