ETAPS 2014: 5-13 April 2014, Grenoble, France
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
Foundations for system design
Organizers: Saddek Bensalem (Verimag, University of Grenoble, France) Yassine Lakhnech (Verimag, University of Grenoble, France) Axel Legay (INRIA Rennes, France)
Workshop: 6 April 2014
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 2014Final versions for EPTCS: 25 April 2014
Workshop: 12 April 2014
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:
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
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 2014Final 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
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 2014Final versions: 10 February 2014
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):
Besides general software systems, FESCA is interested in methods focusing on a specific application domain, such as:
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
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):
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
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:
Organizer: Dan Ghica (Univ. of Birmingham, UK)
Submission: abstracts max 1 p 25 January 2014Notification: 5 February 2014
Workshop: 12-13 April 2014
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 2014Final versions: 6 February 2014
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
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:
As a summary, topics relevant to the scope of the workshop include (but are not restricted to):
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
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
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
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
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
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)
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 2014Final versions: 10 February 2014
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:
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
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
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:
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
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:
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:
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
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:
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)
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
We have 6 guests and no members online