Workshop Description

Rewriting logic (RL) is a natural model of computation and an expressive semantic framework for concurrency, parallelism, communication, and interaction. It can be used for specifying a wide range of systems and languages in various application fields. It also has good properties as a metalogical framework for representing logics. In recent years, several languages based on RL (ASF+SDF, CafeOBJ, ELAN, Maude) have been designed and implemented. The aim of the workshop is to bring together researchers with a common interest in RL and its applications, and to give them the opportunity to present their recent works, discuss future research directions, and exchange ideas.

The topics of the workshop comprise, but are not limited to,
  • foundations and models of RL;
  • languages based on RL, including implementation issues;
  • RL as a logical framework;
  • RL as a semantic framework, including applications of RL to
    • object-oriented systems,
    • concurrent and/or parallel systems,
    • interactive, distributed, open ended and mobile systems,
    • specification of languages and systems;
  • use of RL to provide rigorous support for model-based software engineering;
  • formalisms related to RL, including
    • real-time and probabilistic extensions of RL,
    • rewriting approaches to behavioral specifications,
    • tile logic;
  • verification techniques for RL specifications, including
    • equational and coherence methods,
    • verification of properties expressed in first-order, higher-order, modal and temporal logics,
    • narrowing-based analysis and verification;
  • comparisons of RL with existing formalisms having analogous aims;
  • application of RL to specification and analysis of
    • distributed systems,
    • physical systems.

Invited speakers

Important Dates

  • Paper submission deadline:
    		•  December 30th 2013
  • Author notification:
    		•  February 2nd 2014
  • Final version informal proceedings:
    		•  February 14th 2014

    Call For Papers

    Available here.

    Submission

    The final program of the workshop will include regular papers, tool papers, and work-in-progress presentations. The program will also contain invited talks to be determined by the program committee. Papers must contain original contributions, be clearly written, include appropriate references, and comparison with related work. They must be unpublished and not submitted simultaneously for publication elsewhere. Tool papers present a new tool, a new tool component, or novel extensions to an existing tool. They should provide a short description of the theoretical foundations with relevant citations, emphasize the design and implementation, and give a clear account of the tool's functionality. The described tools must be publicly available via the web. All submissions should be formatted according to the guidelines for Springer LNCS papers, and should be submitted electronically using EasyChair.

    Regular papers and work-in-progress should not exceed 15 pages including references. Tool papers can have a maximum of 6 pages including references and may have an appendix of up to 4 additional pages with usage details and tool demonstration.

    Proceedings

    All submissions will be evaluated by the Program Committee. Regular papers, tool papers, and work-in-progress that are accepted will be presented at the workshop and included in the proceedings, which will be available during the workshop. Regular papers, tool papers, and invited presentations will also be published in a volume in Springer's Lecture Notes in Computer Science (LNCS) series to be distributed after the workshop.

    Depending on the number and the quality of the contributions, we will consider the preparation of a special issue in some scientific journal in the field with extended versions of a selection of the papers of the workshop.

    Program Committee

    • Mark van den Brand, Eindhoven University of Technology, The Netherlands
    • Roberto Bruni, University of Pisa, Italy
    • Manuel Clavel, IMDEA Software & Universidad Complutense de Madrid, Spain
    • Francisco Durán, Universidad de Málaga, Spain
    • Santiago Escobar (chair), Universidad Politécnica de Valencia, Spain
    • Kokichi Futatsugi, JAIST, Japan
    • Alexander Knapp, Universitat Augsburg, Germany
    • Alberto Lluch-Lafuente, IMT Institute for Advanced Studies Lucca, Italy
    • Dorel Lucanu, Alexandru Ioan Cuza University, Rumania
    • Narciso Martí-Oliet, Universidad Complutense de Madrid, Spain
    • José Meseguer, University of Illinois at Urbana-Champaign, USA
    • Ugo Montanari, University of Pisa, Italy
    • Pierre-Etienne Moreau, Ecole des Mines de Nancy & INRIA Nancy, France
    • Kazuhiro Ogata, JAIST, Japan
    • Peter Ölveczky, University of Oslo, Norway
    • Miguel Palomino, Universidad Complutense de Madrid, Spain
    • Grigore Rosu, University of Illinois at Urbana-Champaign, USA
    • Vlad Rusu, INRIA Lille Nord-Europe, France
    • Mark-Oliver Stehr, SRI International, USA
    • Carolyn Talcott, SRI International, USA
    • Martin Wirsing, Ludwig Maximilians Universität München, Germany

    Steering Committee

    • Kokichi Futatsugi, JAIST, Japan
    • Claude Kirchner, INRIA Research Center Bordeaux - Sud-Ouest, France
    • Narciso Martí-Oliet, Universidad Complutense de Madrid, Spain
    • José Meseguer, University of Illinois at Urbana-Champaign, USA
    • Ugo Montanari, University of Pisa, Italy
    • Grigore Rosu, University of Illinois at Urbana-Champaign, USA
    • Carolyn Talcott, SRI International, USA
    • Martin Wirsing, Ludwig Maximilians Universität München, Germany

    Accepted papers

    Regular papers

    1. Luis Aguirre, Narciso Marti-Oliet, Miguel Palomino and Isabel Pita. Conditional Narrowing Modulo in Rewriting Logic and Maude
    2. Thomas Genet. Towards Static Analysis of Functional Programs using Tree Automata Completion
    3. Camilo Rocha, José Meseguer and Cesar Munoz. Rewriting Modulo SMT and Open System Analysis
    4. Kyungmin Bae and Jose Meseguer. Infinite-State Model Checking of LTLR Formulas Using Narrowing
    5. Si Liu, Peter Csaba Ölveczky and José Meseguer. A Framework for Mobile Ad hoc Networks in Real-Time Maude
    6. Mu Sun and José Meseguer. Formal Specification of Button-Related Fault-Tolerance Micropatterns
    7. Min Zhang, Yunja Choi and Kazuhiro Ogata. A Formal Semantics of the OSEK/VDX Standard in K Framework and its Applications
    8. Salvador Lucas and Jose Meseguer. Strong and Weak Operational Termination of Order-Sorted Rewrite Theories
    9. Salvador Lucas and Jose Meseguer. 2D Dependency Pairs for Proving Operational Termination of CTRSs
    10. Adrian Riesco. An integration of CafeOBJ into Full Maude
    11. Massimo Bartoletti, Maurizio Murgia, Alceste Scalas and Roberto Zunino. Modelling and verifying contract-oriented systems in Maude
    12. Peter D. Mosses and Ferdinand Vesely. FunKons: Component-Based Semantics in K
    13. Andrei Arusoaie, Dorel Lucanu, Vlad Rusu, Traian Florin Serbanuta, Grigore Rosu and Andrei Stefanescu. Language Definitions as Rewrite Theories

    Work-in progress

    1. Mu Sun, José Meseguer and Lui Sha. A Formal Heartbeat Pattern for Open-Loop Safety of Networked Medical Devices
    2. Dominik Klein. Key-Secrecy of PACE with OTS/CafeOBJ
    3. Si Liu, Muntasir Raihan Rahman, Stephen Skeirik, Indranil Gupta and José Meseguer. Formal Modeling and Analysis of Cassandra in Maude
    4. Irina Mariuca Asavoae, Mihail Asavoae and Adrian Riesco. Towards a Formal Semantics-Based Technique for Interprocedural Slicing
    5. Nissreen El-Saber and Artur Boronat. Formalization and Verification of BPMN Models using Maude
    6. Lenz Belzner. Value Iteration for Relational MDPs in Rewriting Logic
    7. Andrew Cholewa, Fan Yang, Catherine Meadows and Jose Meseguer. Maude-PSL : Reconciling Intuitive and Formal Specification in Cryptographic Protocol Analysis

    Program and proceedings

    The program of the workshop is available here. The official one can be found here, and the detailed one with information on all the ETAPS workshops here.  The proceedings are available as a single pdf.