ETAPS 2018 Workshops
Workshop Schedule
You can view the detailed workshop programs by clicking the workshop name in the schedule below.
Schedule |
|||
|---|---|---|---|
WORKSHOP |
ROOM |
DATE |
TIME |
| CMCS 2018 | ARISTOTELIS II | SATURDAY 14 APRIL | 08.00 - 19.00 |
| SUNDAY 15 APRIL | 09.00 - 16.30 | ||
| DICE 2018 | ERATO | SATURDAY 14 APRIL | 08.00 - 18.30 |
| SUNDAY 15 APRIL | 09.00 - 18.00 | ||
| GALOP | KALLIOPI | SATURDAY 14 APRIL | 08.00 - 18.00 |
| SUNDAY 15 APRIL | 09.00 - 18.00 | ||
| VerifyThis 2018 | MELPOMENI | SATURDAY 14 APRIL | 08.00 - 19.00 |
| SUNDAY 15 APRIL | 09.00 - 16.00 | ||
| WRLA 2018 | AMFITRION II | SATURDAY 14 APRIL | 08.00 - 17.30 |
| SUNDAY 15 APRIL | 09.00 - 16.30 | ||
| SynCoP 2018 & PV 2018 | AMFITRION I | SATURDAY 14 APRIL | 08.00 - 16.30 |
| SUNDAY 15 APRIL | 09.00 - 14.00 | ||
| MeTRiD 2018 | ARISTOTELIS I | SUNDAY 15 APRIL | 08.00 - 18.00 |
| CREST 2018 | ERATO | FRIDAY 20 APRIL | 08.00 - 18.00 |
| FoMLAS | AMFITRION I | FRIDAY 20 APRIL | 08.00 - 17.30 |
| LiVe 2018 | KALLIOPI | FRIDAY 20 APRIL | 08.00 - 18.00 |
| MARS & VPT | ARISTOTELIS II | FRIDAY 20 APRIL | 08.00 - 17.30 |
| SNR 2018 | MELPOMENI | FRIDAY 20 APRIL | 08.00 - 18.00 |
| VSSE 2018 | AMFITRION II | FRIDAY 20 APRIL | 08.00 - 18.00 |
Pre-satellites |
ETAPS main conference |
Post-satellites |
|
|---|---|---|---|
|
Saturday 14 April |
Sunday 15 April |
Monday 16 April - Thursday 19 April |
Friday 20 April |
| CMCS 2018 | CREST 2018 | ||
| DICE 2018 | FoMLAS | ||
| GALOP | LiVe 2018 | ||
| VerifyThis 2018 | MARS / VPT 2018 | ||
| WRLA 2018 | SNR 2018 | ||
| SynCoP 2018 + PV 2018 | VSSE 2018 | ||
| MeTRiD 2018 | |||
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)
Abstract regular papers: 12 January 2018
Submission regular papers: 19 January 2018
Notification regular papers: 19 February 2018
Camera-ready copy: 26 February 2018
Submission short contributions: 28 February 2018
Notification short contributions: 12 March 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: Bernd Finkbeiner and Samantha Kleinberg
Abstracts due: Feb 2, 2018
Papers due: Feb 7, 2018
Notification: March 9, 2018
Workshop date: April 20, 2018
Papers for post-workshop proceedings due: June 8, 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: Martin Avanzini (University of Innsbruck, Austria)
Submission date: 31 January 2018
Notification date: 25 February 2018
Final papers due: 11 March 2018
Formal methods for ML-based autonomous systems (FoMLAS)
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: 22 January 2018
Notification date: 12 February 2018
Sixth Workshop on Hot Issues in Security Principles and Trust (HotSpot 2018)
Workshop has been cancelled
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 (http://www.dsi.unive.it/IFIPWG1_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: 31 January 2018
Notification date: 9 March 2018
Final papers due: 23 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 2018
Final papers due: 10 March 2018
3rd Workshop on Models for Formal Analysis of Real Systems (MARS 2018) + Sixth International Workshop on Verification and Program Transformation (VPT 2018) (MARS / VPT 2018)
Please note that the above two workshops have joined together (07/02/2018)
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
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
Abstract submission: 16 January, 2018
Paper submission: 22 January 2018
Notification date: 19 February 2018
Final papers due: 25 February 2018
First International Workshop on Methods and Tools for Rigorous System Design (MeTRiD 2018)
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 5 February 2018
Notification date: 1 March 2018 6 March 2018
Final papers due: 26 March 2018
EPTCS proceedings due: 2 June 2018
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
Abstract Submission: 19 January 2018
Paper Submission: 26 January, 2018
Notification date: 18 February, 2018
Final papers due: 03 March, 2018
5th International Workshop on Synthesis of Complex Parameters (SynCoP 2018) + 4th International Workshop on Parameterized Verification (PV 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.
Systems composed of a finite but possibly arbitrary number of identical components occur everywhere from hardware design (e.g. cache coherence protocols) to distributed applications (e.g. client-server applications). Parameterized verification is the task of verifying the correctness of this kind of systems regardless the number of their components. PV is aimed at bringing together researchers working on Parameterized Verification.
Organiser: Loïg Jezequel
Submission date: 15 January 2018
Notification date: 22 January 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
Workshop on Verification and Synthesis for Software Evolution (VSSE2018)
Software is not static. It keeps growing, gradually becomes more complex, but reuses most of code from previous versions. Software verification could mirror the development process, and the tools could take advantage of the efforts already invested in the verification of preceding versions. This workshop focuses on making formal methods practical and their efforts reusable in various stages of software development. Our ultimate goal is to bring together researchers and engineers to ultimately make the process of software development efficient and the software product trustworthy.
Traditionally the workshop consists solely of invited industrial and academic talks which present recent results in incremental verification, relational verification, regression verification, program equivalence, program repair, and the adjacent areas.
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
Abstract submission: 8 January 2018
Paper submission: 15 January, 2018