ETAPS 2013: 16-24 March 2013, Rome, Italy

ETAPS 2013 Workshops

8th Workshop on Applied and Computational Category Theory (ACCAT)

Category theory is a well-known mathematical modeling language with a wide area of applications in mathematics and computer science, including especially the semantical foundations of topics in software science and development. It is the intention of the ACCAT workshop to bring together leading researchers in the field of ACCAT with those in software science and development in order to transfer categorical concepts and theories in both directions.

Fabio Gadducci (University of Pisa, Italy)
Ulrike Golas (Konrad-Zuse-Zentrum für Informationstechnik Berlin, Germany)

Dates: Sunday March 17th, 2013


1st Workshop on Advances in Systems of Systems (AiSoS)

System-of-Systems describes the large scale integration of many independent self-contained systems to satisfy global needs or multi-system requests.  Examples are smart grid, intelligent buildings, smart cities, transport systems, etc.
There is a need for new modeling formalisms, analysis methods and tools to help make trade-off decisions during design and evolution avoiding leading to sub-optimal design and rework during integration and in service. The workshop should focus on the modeling and analysis of System of Systems.
The workshop Advances in Systems of Systems aims to gather people from different communities in order to encourage exchange of methods and views. The workshop welcomes submissions on new modeling approaches, analysis technique, tool and case studies.

Kim G. Larsen (Aalborg University, Denmark)
Axel Legay (INRIA Renne, France and Aalborg University, Denmark)
Ulrik Nyman (Aalborg University, Denmark)

Paper submission: 14 January 2013 (extended)
Notification: 25 January 2013
Camera ready: 15 February 2013

Dates: Saturday March 16th, 2013


2nd International Workshop on Bidirectional Transformations (BX)

The aim of the workshop is to bring together researchers, established and new, interested in bidirectional transformations from different perspectives, such as: language-based approaches, software/model transformations, data/schema co-evolution. Bidirectional transformations (bx) are a mechanism for maintaining the consistency of at least two related sources of information. Such sources can be databases, software models, documents, graphs, and trees. The methodologies used range from classical program transformation to graph transformation techniques, from ad-hoc techniques for data synchronization to the development of domain-specific languages.

Perdita Stevens (University of Edinburgh, UK)
James Terwilliger (Microsoft, USA)

Paper submission: 18 December 2012
Notification: 22 January 2013
Camera ready: 3 February 2013

Dates: Sunday March 17th, 2013


8th Workshop on Bytecode Semantics, Verification, Analysis and Transformation (Bytecode)

Bytecode, such as produced by, e.g., Java and .NET compilers, has become an important topic of interest, both for industry and academia. The industrial interest stems from the fact that bytecode is typically used for Internet and mobile device applications (smart cards, phones, etc.), where security is a major issue. Moreover, bytecode is device-independent and allows dynamic loading of classes, which provides an extra challenge for the application of formal methods. Also the unstructuredness of the code and the pervasive presence of the operand stack provide further challenges for the analysis of bytecode. This workshop will focus on theoretical and practical aspects of semantics, verification, analysis, certification and transformation of bytecode.

Miguel Gomez-Zamalloa (Univ. of Madrid, Spain)
Germán Puebla (Technical Univ. of Madrid, Spain)

Abstract submission: 16 December 2012
Paper submission: 23 December 2012
Notification: 21 January 2013
Camera ready: 8 February 2013

Dates: Saturday March 23rd, 2013


1st Technical Day on Innovative Techniques on Timing Analysis (CerCo)

The technical day will be focused on innovative techniques on timing analysis of programs. Goal is to make the day an active discussion forum for all non conventional work on timing analysis. In particular, the two European Projects Certified Complexity (CerCo) and Probabilistically Analysable Real-Time Systems (PROARTIS) will present and discuss the respective techniques and results towards improving tightness of WCET estimates in comparison to other timing analysis methods.

The approach investigated in CerCo consists in enhancing compilation to induce on the source language a certified and tight cost model for all O(1) code fragments. This information is then combined with Hoare logic, invariant generators and automatic theorem provers to certify the actual complexity of the program as a function of its arguments (dependent complexity). The technique have been applied to a compiler for C programs (under formal certification in the Matita interactive theorem prover) and a compiler for Lustre programs.

The approach investigated in PROARTIS is the one of Probabilistic Timing Analysis (PTA) that provides WCET bounds with an associated probability of occurrence, known as probabilistic WCET (pWCET) estimates. With PTA, execution timing becomes less dependent on execution history, with drastic reduction in the amount of information required to obtain tight WCET estimates in comparison to other timing analysis methods. PTA can be applied either in a static (SPTA) or measurement-based (MBPTA) manner. MBPTA bases on statistical reasoning, which requires that the random variables describing measurements of end-to-end runs are independent and identically distributed. Independence is obtained by standard statistical techniques. Identical distribution can instead be ensured by construction in PTA-friendly high-performance hardware.

Roberto Amadio (Univ. Paris Diderot, Paris, France)
Claudio Sacerdoti Coen (Univ. di Bologna, Italy)
Ian Stark (The University of Edinburgh, UK)

Dates: Saturday March 23rd, 2013


4th International workshop on Developments in Implicit Computational complExity (DICE)

The area of Implicit Computational Complexity (ICC) grew out from several proposals to use logic and formal methods to provide languages for complexity-bounded computation (e.g., polytime or logspace computation). It aims at studying the computational complexity of programs without referring to external measuring conditions or a particular machine model, but only by considering language restrictions or logical / computational principles entailing complexity properties. Several approaches have been explored for that purpose, like restrictions on primitive recursion and ramification, rewriting systems, linear logic, types and lambda calculus, interpretations of functional and imperative programs. The workshop is intended to be a forum for researchers interested in ICC to present new results and discuss recent developments in this area.

Simona Ronchi della Rocca (Univ. of Torino, Italy)

Dates: Saturday March 16th and Sunday March 17th, 2013


10th International Workshop on Formal Engineering approaches to Software Components and Architectures (FESCA)

One strength of FESCA is the link established between the formal methods community and the software engineering community by exploring how formal approaches can be exploited for the analysis of large software architectures.

We encourage submissions on formal techniques and their application that aid reasoning, analysis and certification of component and servicebased applications. In this context, the following topics are of particular concern:

  • Architecture as a language: Building Domain-Specific Languages (DSLs)
  • Modelling formalisms for the analysis of concurrent, embedded or and model-driven systems assembled of components and services;
  • Modelling formalisms in prediction, analysis and measurement of software quality attributes such as reliability, performance, or security;
  • Properties of component and service-based models
  • Temporal properties (including liveness and safety) and their formal verification;
  • Interface compliance (interface-to-interface and interface-to-implementation) and contractual use of components;
  • Formal methods in Component-Based Software Development
  • Techniques for prediction and formal verification of system properties, including static and dynamic analysis;
  • Instrumentation and monitoring approaches, runtime management of applications;
  • (Semi-) automatic inference of analytical models for existing software systems;
  • Formal methods in Service-Based Software Development
  • Techniques for behaviour modelling of services and their orchestration
  • Static and runtime verification and monitoring techniques for ensuring service quality, such as reliability, security and safety
  • Formal methods in Model-Driven Software Development
  • Abstraction level in modelling formalisms;
  • Safer MDA through integration with formal methods;
  • Correctness of model transformations;
  • Industrial case studies and experience reports.

Submissions concentrating on specification techniques should involve an evaluation of the practical merit of their research and clearly state the analysis and reasoning techniques they enable. We also appreciate work of a formal nature with immediate value to for the industrial context. We encourage not only mature research results, submissions presenting innovative ideas and early results are also of interest.

Barbora Bühnová (Masaryk University, Czech Republic)
Lucia Kapová (Karlsruhe Inst. of Technology, Germany)
Jan Kofroň (Charles Univ. in Prague, Czech Republic)

Dates: Saturday March 23th, 2013

FESCA 2013 KEYNOTE: Vittorio Cortellessa (Università dell'Aquila, Italy), Tradeoff analysis of software quality attributes through optimization models

FESCA 2013 TUTORIAL: Catia Trubiani, Ph.D. (Università dell'Aquila, Italy), Title: Performance antipatterns and feedback in software architectures


2nd Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE)

The topic of the GRAPHITE workshop is graph analysis in all its forms in computer science. Graphs are used to represent data in many application areas, and they are subjected to various computational algorithms in order to acquire the desired information. These graph algorithms tend to have common characteristics, such as duplicate detection to guarantee their termination, independent of their application domain. Over the past few years, it has been shown that the scalability of such algorithms can be dramatically improved by using, e.g., external memory, by exploiting parallel architectures, such as clusters, multi-core CPUs, and graphics processing units, and by using heuristics to guide the search. Novel techniques to further scale graph search algorithms, and new applications of graph search are within the scope of this workshop. Another topic of interest of the event is more related to the structural properties of graphs: which kind of graph characteristics are relevant for a particular application area, and how can these be measured? Finally, any novel way of using graphs for a particular application area is on topic. The goal of this event is to gather scientists from different communities, such as model checking, artificial intelligence planning, game playing, and algorithm engineering, who do research on graph search algorithms, such that awareness of each others' work is increased.

We encourage submission of works which include but are not limited to the following topics:

  • Algorithms for the verification of hardware and software based on graph exploration (e.g. the computation of an explicit state space based on an implicit description)
  • Application of graph based techniques originating in one application domain, applied on a problem in another domain (e.g. verification algorithms on artificial intelligence problems)
  • Techniques to deal with potentially infinite graphs and infinite families of graphs
  • Innovative or otherwise particularly significant case studies of applications of graph based methods
  • Theoretical results on the limits and possibilities of graph based methods
  • Parallel algorithms for graph exploration for distributed and shared memory systems (e.g. clusters, multi-core CPUs, GPGPUs)
  • Graph algorithms in artificial intelligence; planning; game playing; social network analysis; biological network analysis, and similar
  • Graph minimisation and abstraction techniques as a preprocessing step for analysis (e.g. bisimulation reduction, transitive reduction)
  • Computation on graphs through graph transformation techniques
  • I/O Efficient graph algorithms using external memory

Papers on applications and papers bridging multiple application domains are strongly encouraged.

Anton Wijs (Eindhoven Univ. of Technology, Netherlands)
Dragan Bošnački (Eindhoven Univ. of Technology, Netherlands)
Stefan Edelkamp (Univ. of Bremen, Germany)

Dates: Sunday March 24th, 2013


12th International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT)

GT-VMT 2013 is the twelfth workshop of a series that serves as a forum for all researchers and practitioners interested in the use of visual notations (especially graph-based), techniques and tools for the specification, modeling, validation, manipulation and verification of complex systems. The aim of the workshop is to promote engineering approaches that provide effective sound tool support for visual modeling languages, enhancing formal reasoning at the syntactic as well as semantic level (e.g., for model specification, model analysis, model transformation, and model consistency management) in different domains, such as UML, Petri Nets, Graph Transformation or Business Process/Workflow Models.

This year's workshop has a special theme of the analysis of non-functional / extra-functional / quality properties like performance, realtime, safety, reliability, energy consumption. We particularly encourage submissions that focus on the definition and the evaluation of such properties using visual/graph specification techniques, ranging from underlying theory through to their utility in complex system design.

As a summary, topics relevant to the scope of the workshop include (but are not restricted to) the following:

  • visual languages definition and syntax (incl. meta-modelling, grammars and graphical parsing);
  • static and dynamic semantics of visual languages (incl. OCL, graph constraints, simulation, animation, compilation);
  • visual/graph-based analysis in software engineering (incl. testing, verification & validation, static & dynamic analysis techniques);
  • visual/graph constraints (incl. definition, expressiveness, analysis techniques involving constraints);
  • model transformations and their application in model-driven development (incl. in particular, transformations between graphical and textual formalisms);
  • visual modeling techniques and graph transformation applied to patterns;
  • visual modeling techniques and graph transformation applied to novel architectural paradigms (e.g. service-oriented, GRID, and P2P computing, context-aware and adaptive applications, etc.) and to domains such as engineering, biology, and medicine;
  • case studies and novel application areas;
  • tool support and efficient algorithms.


Matthias Tichy (Chalmers Technical University and Gothenburg University, Gothenburg, Sweden)
Leila Ribeiro (Univ. Federal do Rio Grande do Sul, Porto Alegre, Brazil)

Abstract submission: 16 december 2012
Paper submission: 21 december 2012
Notification: 18 January 2013
Camera ready: 1 February 2013

Dates: Saturday March 23th, 2013 and Sunday March 24th, 2013


3rd Workshop on Hybrid Autonomous Systems (HAS)

The interest on autonomous systems is increasing both in industry and academia. Such systems must operate with limited human intervention in a changing environment and must be able to compensate for significant system failures without external intervention. The most appropriate models of autonomous systems can be found in the class of hybrid systems (which study continuous-state dynamic processes via discrete-state controllers) that interact with their environment. This workshop brings together researchers interested in all aspects of autonomy and resilience of hybrid systems.

Manuela Bujorianu (Warwick University, UK)
Giordano Pola (Univ. of L'Aquila, Italy)
Luca Bortolussi (Univ. of Trieste, Italy)

Paper submission: 20 december 2012

Dates: Sunday March 17th, 2013


1st Workshop on Hot issues in Security Principles and Trust (Hot-Spot)

This workshop is intended to be a less formal counterpart to the Principles of Security and Trust (POST) conference at ETAPS, and with an emphasis on "hot topics", both of security and of its theoretical foundations and analysis.
Like POST, the themes are

  • theory of computer security;
  • formal specification, analysis and design of security systems;
  • automated reasoning for security analysis.

Submissions about new and emerging topics (for example, those that have not appeared prominently in conferences and workshops until now) are particularly encouraged. Submissions of preliminary, tentative work are also encouraged. There is no page limit, but the length of your submission should be appropriate to its content. There will be no formal proceedings. Inclusion in informal proceedings is optional.

Mark Ryan (University of Birmingham, UK)

Submission: 4 January 2013
Notification: 25 January 2013
Final version for informal proceedings (optional): 22 February 2013

Dates: Sunday March 17th, 2013


21st Meeting of IFIP WG1.3 Foundations of System Specification (IFIP WG1.3)

Aims: To support and promote the systematic development of the fundamental mathematical theory of systems specification. To investigate the theory of formal models for systems specification, development, transformation and verification.

Scope: The theoretical aspects of the specification and development of computing systems that are based on algebraic and logical concepts, and can be studied systematically within a theory of systems specification.

Till Mossakowski (University of Bremen, Germany)

Dates: Saturday March 16th, 2013


8th Workshop on Model-Based Testing (MBT)

MBT 2013 is devoted to model-based testing of both software and hardware. Model-based testing uses models that describe the behavior of the system under consideration to guide such efforts as test selection and test results evaluation. Model-based testing has gained attention with the popularization of models in software/hardware design and development. Of particular importance are formal models with precise semantics, such as state-based formalisms. Testing with such models allows one to measure the degree of the product's conformance with the model. The intent of this workshop is to bring together researchers and users using different kinds of models for testing and to discuss the state of the art in theory, applications, tools, and industrialization of model-based testing.

Alexander K. Petrenko (Moscow State University, Moscow, Russia)
Holger Schlingloff (Fraunhofer FOKUS and Humboldt-Universität, Berlin, Germany)

Dates: Sunday March 17th, 2013


MEALS Workshop

Computing systems are getting ever more ubiquitous, making us dependent on their proper functioning. MEALS is a European research project under IRSES Exchange Programme focused on designing and developing methods which provide a formal approach to model, understand, and analyze systems, wrt their required behavior: correct (i.e. they conform their intended behaviour), safe (i.e. its operation does not have catastrophic consequences), reliable, available to provide the intended service, and secure (i.e., no user without appropriate clearance can access or modify protected data).

The purpose of this workshop arranged by MEALS is to bring researchers, practitioners and industry together to discuss the issues, challenges and latest solutions for formal techniques for the specification, verification and synthesis of dependable ubiquitous computing systems, with respect to both qualitative (i.e. pure non-deterministic models) as well as quantitative behaviour (i.e. extended with probabilistic information). The workshop is targeted towards researchers interested in formal methods in all their aspects: foundations (their mathematical and logical basis), algorithmic advances (the conceptual basis for software tool support) and practical considerations (tool construction and case studies). The workshop will feature a number of distinguished presentations on newest challenges, new techniques, case studies, and tool demonstrations.

Suzana Andova (Eindhoven Univ. of Technology, The Netherlands)
Pedro R. D'Argenio (Univ. Nacional de Cordoba, Argentina)

Dates: Sunday March 17th, 2013


5th Meeting of the working group on Models and Logics for Quantitative Analysis (MLQA)

Models and Logics for Quantitative Analysis are seen as comprising process models that are analysed using logics for quantitative properties. More specifically, we consider process models formally described by transition systems, automata or process calculi, and we consider logics for expressing stochastic and continuous properties as well as discrete ones, we focus on algorithms, theory and tools, and study applications with particular emphasis on embedded systems and service oriented systems but will aim at treating also IT guided workflow systems and biological systems.

The proposed theme for MLQA 2013 is Cyber Physical Systems.

Flemming Nielson (Techn. Univ. of Denmark, Lyngby, Denmark)

Dates: Sunday March 24th, 2013


5th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES)

Applications today are built using numerous interacting services; soon off-the-shelf CPUs will host thousands of cores, and sensor networks will be composed from a large number of processing units. Many applications need to make effective use of thousands of computing nodes. At some level of granularity, computation in such systems is inherently concurrent and communication-centred. PLACES aims to offer a forum where researchers from different fields exchange new ideas on one of the central challenges for programming in the near future, the development of programming methodologies and infrastructures where concurrency and distribution are the norm rather than a marginal concern.

Submissions are invited in the general area of foundations of programming languages for concurrency, communication and distribution. Specific topics include:

  • language design and implementations for communications and/or concurrency
  • session types
  • concurrent data types
  • concurrent objects and actors
  • multicore programming
  • use of message passing in systems software
  • integration of sequential and concurrent programming
  • interface languages for communication and distribution
  • program analysis
  • web services
  • novel programming methodologies for sensor networks
  • high-level programming abstractions for security concerns in concurrent, distributed programming
  • runtime architectures for concurrency, scalability and/or resource allocations


Papers are welcome which present novel and valuable ideas as well as experiences.

Nobuko Yoshida (Imperial College London, UK)
Wim Vanderbauwhede (University of Glasgow, UK)

Abstract submission: 14 December 2012
Paper submission: 21 December 2012
Notification: 23 January 2013
Camera ready: 4 February 2013

Dates: Saturday March 23th, 2013


11th Workshop on Quantitative Aspects of Programming Languages (QAPL)

Quantitative aspects of computation refer to the use of physical quantities (time, bandwidth, etc.) as well as mathematical quantities (for example, probabilities) for the characterisation of the behaviour and for determining the properties of systems. Such quantities play a central role in defining both the model of systems (architecture, language design, semantics) and the methodologies and tools for the analysis and verification of system properties. The aim of the QAPL workshop series is to discuss the explicit use of time and probability and general quantities either directly in the model or as a tool for the analysis of systems.

Luca Bortolussi (Univ. of Trieste, Italy)
Herbert Wiklicky (Imperial College London, UK)

Abstract submission: 16 December 2012
Paper submission: 20 December 2012
Notification: 20 January 2013
Camera ready: 3 February 2013

Dates: Saturday March 23th, 2013 and Sunday March 24th, 2013


1st International Workshop on Strategic Reasoning (SR)

Strategic reasoning is one of the most active research area in multi-agent system domain. The literature in this field is extensive and provides a plethora of logics for modeling strategic ability. Theoretical results in this area are now being used in many exciting domains, including software tools for information system security, robot teams with sophisticated adaptive strategies, and automatic players capable of beating expert human adversary, to cite a few. All these examples share the challenge of developing novel theories and tools for agent strategies that take into account the likely behavior of adversaries.
This workshop aims to bring together researchers working on different aspects of strategic reasoning, both from a theoretical and a practical point of view.

The topics covered by the conference include, but are not limited to, the following:

  • Logics for reasoning about strategic abilities
  • Logics for multi-agent mechanism design, verification, and synthesis
  • Logical foundations of decision theory for multi-agent systems
  • Strategic reasoning in formal verification
  • Automata Theory for strategy sinthesis
  • Strategic reasoning under perfect and imperfect information
  • Applications and tools for cooperative and adversarial reasoning
  • Robust planning and optimization in multi-agent systems
  • Risk and uncertainty in multi-agent systems
  • Quantitative aspects in strategic reasonings


Aniello Murano (Univ of Napoli Federico II, Naples, Italy)
Fabio Mogavero (Univ of Napoli Federico II, Naples, Italy)
Moshe Y. Vardi (Rice University, Houston, USA)

Abstract submission: 15 December 2012
Paper submission: 20 December 2012
Notification: 17 January 2013
Camera ready: 31 January 2013

Dates: Saturday March 16th, 2013 and Sunday March 17th, 2013


7th International Workshop on Computing with Terms and Graph (TERMGRAPH)

The advantage of computing with graphs rather than terms is that common subexpressions can be shared, improving the efficiency of computations in space and time. Sharing is ubiquitous in implementations of programming languages : many functional, logic, object-oriented and concurrent calculi are implemented using term graphs. Research in term and graph rewriting ranges from theoretical questions to practical implementation issues. Different research areas include: the modelling of first- and higher-order term rewriting by (acyclic or cyclic) graph rewriting, the use of graphical frameworks such as interaction nets and sharing graphs (optimal reduction), rewrite calculi for the semantics and analysis of functional programs, graph reduction implementations of programming languages, graphical calculi modelling concurrent and mobile computations, object-oriented systems, graphs as models of biological or chemical abstract machines, and automated reasoning and symbolic computation systems working on shared structures.

Rachid Echahed (IMAG, Grenoble, France)
Detlef Plump (Univ. of York, UK)

Dates: Saturday March 23th, 2013


2nd Workshop on Validation Strategies for Software Evolution (VSSE)

This workshop focuses on verification and testing of software change and upgrades. Software is usually not written all at once, but is built incrementally, due to several reasons:

  • Maintenance (fixing errors and flaws, hardware changes, etc.)
  • Enhancements (new functionality, improved efficiency, extension, new regulations, etc.)

Changes are done frequently during the lifetime of most systems and can introduce software errors that were not present in the old version, or expose errors that were present before but did not get exercised. In addition, upgrades are done gradually, so the old and new versions have to co-exist in the same system. This workshop will address the issue of efficient and reliable verification of system changes and upgrades by means of formal verification and dynamic analysis techniques.

Hana Chockler (IBM Research, Haifa, Israel)
Giovanni Denaro (Univ. of Milano Bicocca, Italy)
Daniel Kroening (Oxford Univ., UK)
Leonardo Mariani (Univ. of Milano Bicocca, Italy)
Natasha Sharygina (Univ. of Lugano, Switzerland)

Paper submission: 20 December 2012
Author notification: 20 January 2013
Camera ready version: 30 January 2013

Dates: Saturday March 16th, 2013