ETAPS 2018 Workshops

Workshop Schedule (coming soon)

The Detailed Workshop Programme will be available as a pdf (coming soon). All workshops will be located at: TBA

14th IFIP WG 1.3 International Workshop on Coalgebraic Methods in Computer Science (CMCS 2018)

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 workshop is to bring together researchers with a common interest in the theory of coalgebras, their logics, and their applications.

Organiser: Corina Cirstea (University of Southampton, United Kingdom)

Submission date: 13 January 2018 
Notification date: 12 February 2018 
Final papers due: 19 February 2018 

3rd Workshop on formal reasoning about Causation, Responsibility, and Explanations in Science and Technology (CREST 2018)

CREST 2018 is the third in a series of workshops addressing formal approaches to reasoning about causation in systems engineering. The topic of formally identifying the cause(s) of specific events - usually some form of failures -, and explaining why they occurred, are increasingly in the focus of several, disjoint communities. The main objective of CREST is to bring together researchers and practitioners from industry and academia in order to enable discussions how explicit and implicit reasoning about causation is performed. A further objective is to link to the foundations of causal reasoning in the philosophy of sciences and to causal reasoning performed in other areas of computer science, engineering, and beyond.

Organisers: Gregor Gössler (INRIA, France), Oleg Sokolsky (University of Pennsylvania, United States)

Submission date: 15 January 2018 
Notification date: 15 February 2018 
Final papers due: 15 March 2018 
EPTCS proceedings due: 1 September 2018

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

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. Ptime, 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.

Organiser: Patrick Baillot (Université de Lyon, France)

Submission date: 31 January 2018 
Notification date: 25 February 2018 
Final papers due: 11 March 2018 

Formal Approaches towards Accountability, Explainability, and Predictability of Autonomous Systems

After the well-known DARPA Urban challenge, there have been significant improvements towards autonomous driving. In the past few years, the major theme when building self-driving cars has shifted to deep learning and probabilistic techniques. When these new algorithms act as key components in autonomous driving, they create substantial technological challenges in terms of explainability (e.g., can I explain what is happening inside the machine-learning algorithm?), predictability (e.g., can I predict what will happen next in the algorithm, or how good can the machine learning component generalize?), and accountability (e.g., when an accident occurs, can one find the root cause, or who is the one to blame?). This goal of this workshop is to facilitate discussion regarding how formal methods can be used to increase predictability, explainability, and accountability of autonomous systems. The workshop welcomes results from concept formulation (by connecting these concepts with existing research topics in logic and games), as well as algorithms, tools or concrete case studies.

Organisers: Chih-Hong Cheng , Indranil Saha 

Submission date: 10 February 2018 
Notification date: 3 March 2018 
Final papers due: 24 March 2018
EPTCS proceedings due: 1 May 2018

International Workshop on Games for Logic and Programming Languages (GALOP)

GaLoP is an annual international workshop on game-semantic models for logics and programming languages and their applications. This is an informal workshop that welcomes work in progress, overviews of more extensive work, programmatic or position papers and tutorials.

This is an established ETAPS workshop, which has been running for the past 12 years.

Organiser: Dan R. Ghica

Submission date: 30 January 2018 
Notification date: 9 February 2018 
Final papers due: 9 February 2018 

Sixth Workshop on Hot Issues in Security Principles and Trust (HotSpot 2018)

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.

As the previous four issues, the edition will be part of the activities of the IFIP WG 1.7 ( on Theoretical Foundations of Security Analysis and Design.

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 (typically, those that have not appeared prominently in conferences and workshops until now, but also recent additional results) 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.

Organiser: Riccardo Focardi 

Submission date: 19 January 2018 
Notification date: 2 March 2018 
Final papers due: 16 March 2018 

2nd Workshop on Learning in Verification (LiVe 2018)

The success of machine learning has recently motivated researchers in formal methods to adapt the highly scalable learning methods to the verification setting, where correctness guarantees on the result are essential.

The aim of this workshop is to bring together researchers from the formal verification community that are developing approaches to exploit learning methods in verification as well as researchers from machine learning area interested in applications in verification and synthesis.

The topic includes any use of learning techniques to speed up or enhance verification, for example reinforcement learning in the analysis of complex systems, decision-tree learning for generating invariants of programs or computing small and understandable counterexamples and controllers, or the meta-usage for predicting best tools to be applied to a verification problem.

Organiser: Jan Kretinsky 

Submission date: 2 February 2018 
Notification date: 27 February 2017 
Final papers due: 10 March 2017 

3rd Workshop on Models for Formal Analysis of Real Systems (MARS 2018)

Specification formalisms and modelling techniques are often developed with formal analysis and formal verification in mind. To demonstrate applicability, tiny case studies are typically presented in research papers. But to show that a developed approach actually scales to real systems, large case studies are essential. The process of developing a detailed and accurate model usually takes a considerable amount of time, often months to years.

This workshop emphasises modelling. In particular, we invite papers that present full models of real systems, which may lay the basis for future comparison and analysis. By default, the models related to the submission will be archived in a repository in a machine-readable form. The workshop brings together researchers from different communities facing real systems and developing formal models thereof, especially in areas where large models occur, such as networked or cyber-physical systems. An aim of the workshop is to present different modelling approaches, to discuss pros and cons for each of them, and to start a collection of interesting benchmarks for diverse formal methods.

Organisers: Rob van Glabbeek , Wendelin Serwe 

Submission date: 12 January 2018 
Notification date: 19 February 2018 
Final papers due: 12 March 2018 
EPTCS proceedings due: 26 March 2018

First International Workshop on Methods and Tools for Rigorous System Design (MeTRiD 2017)

Modern software systems are inherently concurrent. They consist of components running simultaneously and sharing access to resources provided by the execution platform. This leads to resource contention and potential deadlocks compromising mission- and safety-critical operations. Similar problems are observed in various kinds of software, including system, work-flow management, integration software, web services etc. Essentially, any software entity that goes beyond simply computing a certain function, necessarily has to interact and share resources with other such entities.

The intrinsic concurrent nature of such interactions is the root cause of the sheer complexity of the resulting software, which is exponential in the number of components, making complete a posteriori verification practically infeasible. An alternative approach consists in ensuring correctness by construction.

The Rigorous System Design approach is based on a formal, accountable and iterative process for deriving trustworthy and optimized implementations from models of application software, its execution platform and its external environment. A system implementation is derived from a set of appropriate high-level models by applying a sequence of semantics-preserving transformations.

Organisers: Saddek Bensalem , Simon Bliudze 

Submission date: 28 January 2018 
Notification date: 1 March 2018 
Final papers due: 26 March 2018 
EPTCS proceedings due: 2 June 2017

The 4th International Workshop on Symbolic and Numerical Methods for Reachability Analysis SNR 2018)

Hybrid systems are complex dynamical systems that combine discrete and continuous components. Reachability questions, regarding whether a system can run into a certain subset of its state space, are at the core of verification and synthesis problems for hybrid systems.

There are several successful methods for hybrid systems reachability analysis. Some methods explicitly construct flow-pipes that over-approximate the set of reachable states over time, where efficient computation of such over-approximations requires symbolic representations, such as support functions. Other methods based on satisfiability checking technologies symbolically encode reachability properties as logical formulas, while solving such formulas requires numerically-driven decision procedures. Last but not least, automated deduction and the usage of theorem provers have led to efficient analysis approaches. The goal of this workshop is to bring together researchers working with different reachability analysis techniques and to seek for synergies between the different approaches.

Organisers: Taylor T. Johnson , Martin Fränzle 

Submission date: 3 January 2018 
Notification date: 11 February 2018 
Final papers due: 18 February 2018 
EPTCS proceedings due: 28 February 2018

5th International Workshop on Synthesis of Complex Parameters (SynCoP 2018)

SynCoP aims at bringing together researchers working on verification and parameter synthesis for systems with discrete or continuous parameters, in which the parameters influence the behavior of the system in ways that are complex and difficult to predict. Such problems may arise for real-time, hybrid or probabilistic systems in a large variety of application domains. The parameters can be continuous (e.g., timing, probabilities, costs) or discrete (e.g., number of processes). The goal can be to identify suitable parameters to achieve desired behavior, or to verify the behavior for a given range of parameter values.

Organiser: Loïg Jezequel 

Submission date: 15 January 2018 
Notification date: 20 February 2018 
Final papers due: 20 March 2018 

VerifyThis Verification Competition 2018 at ETAPS 2018 (VerifyThis2018)

VerifyThis is a series of program verification competitions held earlier at FoVeOOS2011, FM2012, Dagstuhl (April 2014), ETAPS 2015-2017.

The aims of the competition are:
- to bring together those interested in formal verification, and to provide an engaging, hands-on, and fun opportunity for discussion
- to evaluate the usability of logic-based program verification tools in a controlled experiment that could be easily repeated by others.

The competition will offer a number of challenges presented in natural language and pseudo code. Participants have to formalize the requirements, implement a solution, and formally verify the implementation for adherence to the specification.

There are no restrictions on the programming language and verification technology used. The correctness properties posed in problems will have the input-output behavior of programs in focus. Solutions will be judged for correctness, completeness, and elegance.

Organisers: Marieke Huisman , Rosemary Monahan , Peter Müller 

Sixth International Workshop on Verification and Program Transformation (VPT 2018)

The workshop aims to bring together researchers working in the fields of Program Verification and Program Transformation. Recent research in these areas has shown a great potential for beneficial interactions. On one hand, methods and tools for Program Transformation such as partial evaluation, fold/unfold transformations, and supercompilation, have all been applied with success for the verification of infinite state and parameterized systems. On the other hand, model checking, abstract interpretation, SAT and SMT solvers, and automated theorem provers have been used to enhance program transformation techniques. Moreover, the formal certification of tools, such as compilers and automated refactoring tools, has recently attracted considerable interest and posed new challenges. The workshop will also provide a forum where researchers from these fields may interact and foster new developments.

Organisers: John Gallagher , Alexei Lisitsa , Andrei Nemytykh 

Submission date: 22 January 2018 
Notification date: 19 February 2018 
Final papers due: 25 February 2018 
EPTCS proceedings due: 31 May 2018

Workshop on Verification and Synthesis for Software Evolution (VSSE2018)

This workshop focuses on verification of software changes and upgrades, as well as on synthesizing new program versions and automated bug fixing. Software continuously evolves to meet rapidly changing human needs. Each evolved transformation of a program is expected to preserve important correctness and security properties. Thus there is a clear need for the techniques to formally verify program correctness after a change and either provide a proof of correctness or further employ results of performed analysis to fix detected bugs. This workshop will bring together researchers in formal verification and program synthesis to ultimately make the process of software evolution safe.

Organisers: Grigory Fedyukovich 

Submission date: invitation only 
Notification date: invitation only 
Final papers due: invitation only 

12th International Workshop on Rewriting Logic and its Applications (WRLA 2018)

Rewriting logic (RWL) is a natural model of computation and an expressive semantic framework for concurrency, parallelism, communication, and interaction. RWL can be used for specifying a wide range of systems and languages in various application fields. It also has good properties as a meta-logical framework for representing various logics. Moreover, RWL has influenced, in various degrees, the design of several languages and associated toolsets (Maude, Elan, ASF+SDF, CafeOBJ, K). The aim of the workshop is to bring together researchers with a common interest in RWL and its applications, and to give them the opportunity to present their recent works, discuss future research directions, and exchange ideas.

Organiser: Vlad Rusu 

Submission date: 5 January 2018 
Notification date: 16 February 2018 
Final papers due: 6 March 2018 

Who's online

We have 140 guests and no members online

Site Hosted by