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 resultingfrom 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 programing theory to systems
Foundations for system design
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.
Axel Legay (INRIA Rennes, France) Ulrik Nyman (Aalborg University, Denmark)
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:
Kim G. Larsen (Aalborg University, Denmark) Doron Peled (Bar Ilan University, Israel) Nicolas Markey (LSV/CNRS, France)
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.
Marcello Bonsangue (LIACS, The Netherlands)
Abstract regular papers: 6 January 2014 Submission regular papers: 10 January 2014 (strict) Notification regular papers: 14 February 2014 Camera-ready copy: 21 February 2014 Submission short contributions: 23 February 2014 (strict) 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.
Ulrich Schöpp (LMU, Germany)
Abstract Submission: 5 January 2014 Notification: 20 January 2014 Workshop: 5-6 April 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".
Barbora Bühnová (Masaryk University, Czech Republic)Lucia Kapová Happe (Karlsruhe Inst. of Technology, Germany) Jan Kofroň (Charles Univ. in Prague, Czech Republic)
Paper registration: 6 December 2013 Submission deadline: 13 December 2013 Notification of acceptance: 20 January 2014 Final versions due: 10 February 2014Workshop: 12 April 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):
Dimitra Giannakopoulou (NASA Ames, USA) Catherine Dubois (ENSIIE, France) Dominique Mery (LORIA, France)
Abstract submission : 18 December 2013 Paper Submission : 23 December 2013 Notification : 27 January 2014 Final version : 10 February 2014 Workshop date: 6 April 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:
Dan Ghica (Birmingham, UK)
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.
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)
Abstract submission: 23 December 2013 Paper submission: 30 December 2013 Acceptance notification: 31 January 2013 Pre-proceedings camera ready due: 10 February 2013 Workshop: 5 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 the International Workshop on Graphical Models for Security 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.
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 deadline: 13 December 2013 Acceptance notification: 24 January 2014 Camera ready version: 6 February 2014 Workshop: 12 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):
Frank Hermann (University of Luxembourg, Luxembourg) Stefan Sauer (Universitat Paderborn, Germany)
Abstract Submission 6 December 2013 Paper Submission : 13 December 2013 Notification to Authors: 17 January 2014 Camera Ready Submission: 31 January 2014 Workshop: 5-6 April 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.
Manuela Bujorianu (Warwick University, UK) Rafael Wisniewski (Aalborg University, Denmark)
Submission deadline: 6 January 2014 Notification of acceptance: 24 January 2014 Final version deadline: 10 February 2014 Workshop: 12-13 April 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
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.
Sebastian Mödersheim (Technical University of Denmark, DTU)
Paper submission: 3 January 2014 Notification: 31 January 2014 Final version for informal proceedings (optional): 14 February 2014 Workshop: 12 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.
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)
Paper submissions : 16 December 16 2013 Notification of acceptance : 24 January 2014 Final versions : 8 February 2014 Workshop : 6 April 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.
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.
Neel Krishnaswami (University of Birmingham, UK)Paul Blain Levy (University of Birmingham, UK)
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.
Vasco Vasconcelos (University of Lisbon) Alastair F. Donaldson (Imperial College, London)
Abstracts: 16 December 2013 5-page paper: 23 December 2013 Notification: 31 January 2014 Final version for pre-proceedings: 7 February 2014 Workshop: TBC
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.
Nathalie Bertrand (Inria Rennes/IRISA, France)Luca Bortolussi (Univ. of Trieste, Italy)
For regular papers: Abstract: 24 December 2013 23:59 GMT Submission: 31 December 2013 23:59 GMT Notification: 3 February 2014 Final version (ETAPS proceedings): 10 February 2014 Final version (EPTCS proceedings): TBA
For presentation reports: Submission: 5 February 2014 Notification: 12 February 2014
Workshop: 12-13 April 2014
[content under construction]
Alain Girault (INRIA, France) Lothar Thiele (ETHZ, Switzerland)
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:
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)
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:
Étienne André (LIPN, France) Goran Frehse (VERIMAG, France)
Submission (abstract) : 13 January 2014 AoE Submission (paper) : 20 January 2014 AoE Notification : 20 February 2014 Camera ready: 15 March 2014 Workshop : 6 April 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.
Hana Chockler (IBM Research Haifa)Giovanni Denaro (UniMiB)Daniel Kroening (Oxford)Leonardo Mariani (UniMiB)Natasha Sharygina (USI)
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.
Santiago Escobar (Universidad Politecnica de Valencia, Spain)
Paper submission deadline: 30 December 2013 Author notification: 2 February 2014 Final version informal proceedings: 14 February 2014Workshop: 5-6 April 2014
We have 18 guests and no members online