ETAPS 2014: 5-13 April 2014, Grenoble, France

ETAPS 2014 Workshops


From Programs to Systems - The Systems Perspective in Computing

ETAPS Workshop in honor of Joseph Sifakis

Grenoble, April 6, 2014

The focus of computing has been continuously shifting from programs to systems over the past decades. Programs can be represented as relations independent from the physical resources needed for their execution. Their behavior is often terminating, deterministic and platform-independent. On the contrary, systems are interactive. They continuously interact with an external environment. Their behavior is driven by stimuli from the environment, which, in turn, is affected by their outputs.

Systems are inherently complex and hard to design owing to unpredictable and subtle interactions with their environment, emergent behaviors, and occasional catastrophic cascading failures, rather than to complex data and algorithms. Compared tofunction software, their complexity is exacerbated by additional factors such as concurrent execution, uncertainty resulting from interaction with unpredictable environments, heterogeneity of interaction between hardware and software, and nonrobustness (small variations in a certain part of the system can have large effects on overall system behavior).

Theory of computation is, by its very nature, of little help for studying systems. Even if we perfectly understand the properties of a program and the properties of a hardware target platform, we have no theory to predict the behavior of the program running on the platform.

The aim of this workshop is to discuss the Systems Perspective in Computing, by addressing the two following issues:

Extending programming theory to systems

  • To what extent can formal techniques for software development be adapted/extended to system development?
  • Program correctness vs. system correctness;
  • Adapting SW engineering techniques to systems engineering;
  • Software modeling vs. system modeling;
  • How software verification techniques can be adapted to deal with quantitative properties?

Foundations for system design

  • Missing results (theory, methods and tools) enabling rigorous system design;
  • Building faithful system models;
  • Adaptive resources management– Mixed criticality systems;
  • Design space exploration;
  • Automated implementation techniques for distributed or many-core platforms.

Organizers: Saddek Bensalem (Verimag, University of Grenoble, France)
Yassine Lakhnech (Verimag, University of Grenoble, France)
Axel Legay (INRIA Rennes, France)

Workshop: 6 April 2014

Website: index.php/2014/workshops?id=164

2nd Workshop on Advances in Systems of Systems  (AiSoS)

AiSoS 2014 has been cancelled!

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.

Organizers: Axel Legay (INRIA Rennes, France)
Ulrik Nyman (Aalborg University, Denmark)

Submission: papers max 20 pp eptcs.cls 31January 2014 (was 10 January 2014,was 6 January)
Notification: 10 February 2014
Final versions for EPTCS: 25 April 2014

Workshop: 12 April 2014


1st Cassting Workshop (Cassting)

Cassting is a European research project funded by the European Commission under the FP7 for Information and Communication Technology. The objective of Cassting is to develop a novel approach for analysing and designing collective adaptive systems in their totality, by setting up a game theoretic framework. Currently, most of the games played on graphs are of the sort "two-player zero-sum", we aim to extend them to "multiple-player non-zero-sum", and show the applicability of the new theory to the analysis and synthesis of interactive computational systems.

Here components are viewed as players, their behaviour is captured by strategies, system runs are plays, and specifications are winning conditions. We will develop formalisms for modelling collective adaptive systems as games, and algorithms for synthesising optimal strategies (and components).

This 1st Cassting workshop continues the line of GASICS workshop. The aim of this workshop is to bring together researchers working on game-related subjects, and to discuss on various aspects of game theory in the fields where it is applied. The workshop will be composed of two invited talks, together with contributed talks on the following (non-exhaustive) list of relevant topics:

  • Adapted notions of games for synthesis of complex interactive computational systems
  • Games played on complex and infinite graphs
  • Games with quantitative objectives
  • Game with incomplete information and over dynamic structures
  • Heuristics for efficient game solving.

Organizers: Kim G. Larsen (Aalborg University, Denmark)
Doron Peled (Bar Ilan University, Israel)
Nicolas Markey (LSV/CNRS, France)

Submission: abstracts max 2 pp 24 January 2014 (extended)
Notification: 31 January 2014

Workshop: 12 April 2014


12th International Workshop on Coalgebraic Methods in Computer Science (CMCS)

In more than a decade of research, it has been established that a wide variety of state-based dynamical systems, like transition systems, automata (including weighted and probabilistic variants), Markov chains, and game-based systems, can be treated uniformly as coalgebras. Coalgebra has developed into a field of its own interest presenting a deep mathematical foundation, a growing field of applications, and interactions with various other fields such as reactive and interactive system theory, object-oriented and concurrent programming, formal system specification, modal and description logics, artificial intelligence, dynamical systems, control systems, category theory, algebra, analysis, etc.

The aim of the CMCS workshops is to bring together researchers with a common interest in the theory of coalgebras, their logics, and their applications. As the workshop serie strives to maintain breadth in its scope, participation by researchers in neighbouring areas is strongly encouraged.

Organizer: Marcello Bonsangue (LIACS, The Netherlands)

Submission regular papers: abstracts deadline cancelled (was 6 January 2014), papers max 20 pp llncs.cls 15 January 2014  (was 10 January)
Notification regular papers: 14 February 2014
Final versions: 21 February 2014
Submission short contributions: max 2 pp llncs.cls  23 February 2014
Notification short contributions: 9 March 2014

Workshop: 5-6 April 2014


5th 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.

Organizer: Ulrich Schöpp (LMU, Germany)

Submission: extended abstracts max 5 pp 5 January 2014
Notification: 20 January 2014
Final versions: 10 February 2014

Workshop: 5-6 April 2014


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

The aim of the FESCA workshop is to bring together both young and senior researchers from formal methods, software engineering, and industry interested in the development and application of formal modelling approaches as well as associated analysis and reasoning techniques with practical benefits for software engineering. In this context, the topics include (but are not limited to):

  • Modelling
    • Modelling formalisms;
    • Models, metamodels and model transformations;
  • Correctness checking
    • Temporal properties and their formal verification;
    • Interface compliance and contractual use of components;
    • Correctness of models, metamodels and model transformations
  • Analysis and prediction of quality attributes
    • Formal prediction and analysis;
    • Static and dynamic analysis;
    • Instrumentation and monitoring approaches;
  • Industrial case studies and experience reports.

Besides general software systems, FESCA is interested in methods focusing on a specific application domain, such as:

  • Cloud environment
  • Mobile and embedded systems
  • Information systems
  • Hardware infrastructures

Prof. Dr. Colin Atkinson, Chair of Software Engineering at University of Mannheim (Germany), has agreed to deliver the FESCA 2014 keynote speech on the topic "Facilitating Formal Views in View-Driven (Orthographic) Software Engineering" and tutorial "Orthographic and Deep Modeling with Melanee".

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

Submission: abstracts 6 December 2013, papers max 15 pp (regular papers) / 10 pp (position papers) / 8 pp (tool demos) eptcs.cls 13 December 2013
Notification: 20 January 2014
Final versions: 10 February 2014

Workshop: 12 April 2014


1st Workshop on Formal Integrated Development (F-IDE)

High levels of safety, security and also privacy standards require the use of formal methods to specify and develop compliant software (sub)systems. Any standard comes with an assessment process, which requires a complete documentation of the application in order to ease the justification of design choices and the review of code and proofs.

Ideally, an F-IDE dedicated to such developments should comply with several requirements. The first one is to associate a logical theory with a programming language, in a way that facilitates the tightly coupled handling of specification properties and program constructs. The second one is to offer a language/environment simple enough to be usable by most developers, even if they are not fully acquainted with higher-order logics or set theory, in particular by making development of proofs as easy as possible. The third one is to offer automated management of application documentation. It may also be expected that developments done with such an F-IDE are reusable and modular. Moreover, tools for testing and static analysis may be embedded in this F-IDE, to help address most steps of the assessment process. The workshop is opened to contributions on various aspects (but not exclusively):

  • F-IDE building : design and integration of languages, compilation
  • How to make high-level logical and programming concepts palatable to industrial developers
  • Integration of object-oriented and modularity features
  • Integration of static analysers
  • Integration of automatic proof tools, theorem provers and testing tools
  • Documentation tools
  • Impact of tools on certification
  • Experience reports of developing F-IDE
  • Experience reports of using F-IDE
  • Experience reports of formal methods-based assessments of industrial applications

Organizers: Dimitra Giannakopoulou (NASA Ames, USA)
Catherine Dubois (ENSIIE, France)
Dominique Mery (LORIA, France)

Submission: abstracts 27 December 2013 (was 18 December), papers 6-14 pp eptcs.cls 30 December 2013 (was 23 December)
Notification: 27 January 2014
Final versions: 10 February 2014

Workshop: 6 April 2014


Games for Logic and Programming Languages IX (GALOP)

This is intended to be an informal workshop. Participants are encouraged to present work in progress, overviews of more extensive  work, and programmatic/position papers, as well as completed projects in the following areas:

  • Game theory and interaction models in semantics
  • Games-based program analysis and verification
  • Logics for games and games for logics
  • Algorithmic aspects of games
  • Categorical aspects
  • Programming languages and full abstraction
  • Higher-order automata and Petri nets
  • Geometry of Interaction
  • Ludics
  • Epistemic game theory
  • Logics of dependence and independence
  • Computational linguistics

Organizer: Dan Ghica (Univ. of Birmingham, UK)

Submission: abstracts max 1 p 25 January 2014
Notification: 5 February 2014

Workshop: 12-13 April 2014


International Workshop on Graphical Models for Security (GraMSec)

Graphical security models provide an intuitive but systematic methodology to analyze security weaknesses of systems and to evaluate potential protection measures. Such models have been subject of academic research and they have also been widely accepted by the industrial sector, as a means to support and facilitate threat analysis and risk management processes.

The objective of GraMSec is to contribute to the development of well-founded graphical security models, efficient algorithms for their analysis, as well as methodologies for their practical usage. The workshop will bring together academic researchers and industry practitioners designing and employing visual models for security in order to provide a platform for discussion, knowledge exchange and collaborations. GraMSec will contribute to bridging a gap between formal foundations and practical requirements, which both need to be addressed in order to develop sound and usable security solutions.

Organizers: Barbara Kordy (University of Luxembourg, Luxembourg)
Wolter Pieters (University of Twente and Delft University of Technology, The Netherlands)
Sjouke Mauw (University of Luxembourg, Luxembourg)

Submission: papers max 15 pp (regular papers) / 5 pp (short papers) eptcs.cls 13 December 2013 (was 6 December)
Notification: 24 January 2014
Final versions: 6 February 2014

Workshop: 12 April 2014


3rd Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE)

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 analyse 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.

Organizers: Anton Wijs (Eindhoven Univ. of Technology, Netherlands)
Dragan Bošnački (Eindhoven Univ. of Technology, Netherlands)
Stefan Edelkamp (Univ. of Bremen, Germany)
Alberto Lluch Lafuente (IMT Institute for Advanced Studies Lucca, Italy)

Submission: abstracts 31 January 2014 (was 6 January 2014,was 23 December 2013), papers max 12 pp eptcs.cls 3 February 2014 (was 10 January 2014, was 30 December 2013)
Notification: 28 February 2014 (was 31 January 2014)
Final versions for pre-proceedings: 15 March 2014 (was 10 February 2014)

Workshop: 5 April 2014


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

GT-VMT 2014 is the thirteenth 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 and 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 special theme is “Reliability” and we particularly encourage submissions that address the following questions:

  • How can graph transformation and visual modelling support the modelling, analysis and/or verification of functional requirements?
  • How can these techniques ensure a certain level of robustness of systems?

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

  • 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 (particularly incl. transformations between graphical and textual formalisms);
  • visual modeling techniques and graph transformations applied to patterns;
  • visual modeling techniques and graph transformations for systems with quality properties like performance, real-time, safety, reliability, energy consumption;
  • case studies and novel application areas (e.g. within engineering, biology, etc.) regarding the above topics;
  • tool support and efficient algorithms for the aforementioned topics.

Organizers: Frank Hermann (University of Luxembourg, Luxembourg)
Stefan Sauer (Universitat Paderborn, Germany)

Submission: abstracts 31 January 2014 papers max 12 pp eceasst.cls 3 February 2014 (was 13 December 2013)
Notification: 28 February 2014
Final versions:  14 March 2014

Workshop: 5-6 April 2014


4th 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.

Organizers: Manuela Bujorianu (Warwick University, UK)
Rafael Wisniewski (Aalborg University, Denmark)

Submission: 17 January 2014
Notification: 24 January 2014
Final versions: 10 February 2014

Workshop: 12 April 2014


2nd 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.

Organizer: Sebastian Mödersheim (Technical University of Denmark, Denmark)

Submission: 10 January 2014 (was 3 January 2014)
Notification: 31 January 2014
Final versions for informal proceedings (optional): 14 February 2014

Workshop: 12 5 April 2014


9th Workshop on Model-Based Testing (MBT)

MBT 2014 is devoted to model-based testing of both software and hardware, as well as new trends in fusion of testing with other model-based verification technologies.

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.

Organizers: Alexander K. Petrenko (Moscow State University, Moscow, Russia)
Holger Schlingloff (Fraunhofer FOKUS and Humboldt-Universität, Berlin, Germany)
Nikolay Pakulin (Institute for System Programming, RAS, Russia)

Submission: papers max 15 pp eptcs.cls 23 December 2013 (was 16 December)
Notification: 24 January 2014
Final versions: 8 February 2014

Workshop: 6 April 2014


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.

Organizers: Axel Legay (INRIA Rennes, France)
Joost-Pieter Katoen (RWTH Aachen University, Germany)

Workshop: 6 April 2014


5th Workshop on Mathematically Structured Functional Programming (MSFP)

The fifth workshop on Mathematically Structured Functional Programming is devoted to the derivation of functionality from structure. It is a celebration of the direct impact of Theoretical Computer Science on programs as we write them today. Modern programming languages, and in particular functional languages, support the direct expression of mathematical structures, equipping programmers with tools of remarkable power and abstraction. Where would Haskell be without monads? Functional reactive programming without arrows? Call-by-push-value without adjunctions?  The list goes on. This workshop is a forum for researchers who seek to reflect mathematical phenomena in data and control. 

Organizers: Neel Krishnaswami (University of Birmingham, UK)
Paul Blain Levy (University of Birmingham, UK)

Submission: abstracts 31 December 2013 (was 24 December), papers (no page limit) eptcs.cls 7 January 2014 (was 31 December 2013)
Notification: 3 February 2014
Final  versions: 10 February 2014

Workshop: 12 April 2014


6th 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.

Organizers: Vasco Vasconcelos (University of Lisbon, Portugal)
Alastair F. Donaldson (Imperial College, UK)

Submission: abstracts deadline cancelled (was 16 December 2013), papers max 5 pp eptcs.cls 3 January 2014 (was 23 December 2013)
Notification: 31 January 2014
Final versions for pre-proceedings: 7 February 2014

Workshop: 12 April 2014


12th 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.

Organizers: Nathalie Bertrand (Inria Rennes/IRISA, France)
Luca Bortolussi (Univ. of Trieste, Italy)

Submission of regular paprers: abstracts  deadline cancelled (was 24 December 2013), papers max 15 pp eptcs.cls 8 January 2014 (was 31 December 2013)
Notification of regular papers: 3 February 2014
Final versions for pre-proceedings: 10 February 2014
Final versions for EPTCS: tba
Submission of presentation reports: paper max 4 pp eptcs.cls 5 February 2014
Notification of presentation reports: 12 February 2014

Workshop: 12-13 April 2014


Workshop on Reconciling Performance with Predictability (RePP)

The RePP workshop targets embedded systems with both efficiency requirements and critical temporal constraints, occurring in many industrial domains: avionics, automotive, railway, energy, and robotics.

Guaranteeing the temporal constraints depends on the predictability properties of the whole system (processor architecture, software, OS, scheduling strategy, communications, and middleware). However, system efficiency is measured by means of average-case behavior with performance, resource utilization, and power consumption criteria.

Reasons for the gap between average-case and worst-case behavior are the variation and non-determinism of the system environment, and the interferences caused by shared resources. Unfortunately, new classes of hardware platforms such as multi-core processors and multiprocessors-on-a-chip as well as the demand for adaptive and multi-mode applications quickly increase system efficiency if worst-case behavior needs to be guaranteed.

The workshop will discuss approaches that attack the improvement of both worst-case predictability and of average-case performance. Topics of interest include mixed-criticality approaches, predictable (multi-core) architectures, worst-case execution time and interference analysis, resource-aware compilers, scheduling and allocation considering worst-case and average-case performance, and certification.

Contributions should relate to the main subject of the workshop. The following issues and questions are of special interest:

  • Concepts and metrics for characterizing predictability.
  • Computer science has been successful in removing resource interactions from interfaces. Does it make sense to enrich interfaces with resource-related information. If yes, on which level of abstraction (instruction set, software components, …).
  • Do resource interactions have an influence across abstraction layers? In particular, can improvements on one layer lead to degradation on another layer?
  • Designing new hardware with special support for predictability.
  • Using mainstream software development for predictability, for instance with the support of new compilers for classical programming languages.
  • Multicore predictable processors: How can embedded multicore processors be designed in a time predictable fashion?
  • Parallel predictable processors: How can embedded control algorithms that require a higher performance than sequential processors can deliver be parallelized and allow for time predictability of the parallel task?
  • Mixed criticality: Is the execution of mixed real-time and non-real-time applications on an embedded multicore processor feasible?
  • Case studies involving applications where one needs to guarantee deadlines AND average performance.

Organizers: Alain Girault (INRIA, France)
Lothar Thiele (ETHZ, Switzerland)

Submission: papers 10-15 pp llncs.cls 14 February 2014 (was 21 January)
Notification: 7 March 2014 (was 21 February)
Final versions: 21 March 2014 (was 14 March)
Workshop: 6 April 2014


2nd 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
Organizers: Fabio Mogavero (Univ of Napoli Federico II, Naples, Italy)
Aniello Murano (Univ of Napoli Federico II, Naples, Italy)
Moshe Y. Vardi (Rice University, Houston, USA)
Submission: abstracts 27 December 2013 (was 16 December), papers max 5 pp eptcs.cls 30 December 2013 (was 23 December)
Notification: 30 January 2014
Final versions: 10 February 2014
Workshop: 5-6 April 2014

1st International Workshop on Synthesis of Continuous Parameters (SynCop)

SynCoP aims at bringing together researchers working on parameter synthesis for systems with continuous variables, where the parameters consist of a (usually dense) set of constant values. Such problems arise for real-time, hybrid or probabilistic systems where the goal is to identify suitable parameters to achieve desired behavior, or to verify the behavior for a given range of parameter values. A parameter could be, e.g., a delay in a real-time system, or a reaction rate in a biological cell model.

The scientific subject of the workshop covers (but is not limited to) the following areas:

  • parameter synthesis,
  • parametric model checking,
  • robustness analysis,
  • formalisms such as parametric timed and hybrid automata, parametric time(d) Petri nets, parametric probabilistic automata,
  • applications to major areas of computer science and control engineering.

Organizers: Étienne André (LIPN, France)
Goran Frehse (VERIMAG, France)

Submission: abstracts deadline cancelled (was 13 January 2014) , papers max 15 pp eptcs.cls 3 February 2014 (was 20 January)
Notification : 27 February 2014 (was 20 February)
Final versions: 15 March 2014

Workshop: 6 April 2014


3rd Workshop on Validation Strategies for Software Evolution (VSSE)

This workshop focuses on verification and testing of software changes 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.

Organizers: Hana Chockler (IBM Research Haifa, Israel)
Giovanni Denaro (UniMiB, Italy)
Daniel Kroening (Univ. of Oxford, UK)
Leonardo Mariani (UniMiB, Italy)
Natasha Sharygina (USI, Switzerland)

Workshop: 5 April 2014


10th International Workshop on Rewriting Logic and Its Applications (WRLA)

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.

Organizer: Santiago Escobar (Universidad Politecnica de Valencia, Spain)

Submission: paper max 15 pp (regular papers)/ 6(+4) pp (tool papers) llncs.cls 30 December 2013
Notification: 2 February 2014
Final versions for pre-proceedings: 14 February 2014

Workshop: 5-6 April 2014