ETAPS 2021 Workshops
NOTICE REGARDING THE TIMES IN THE PROGRAMME: All times are given in Luxembourg time (unless explictly indicated otherwise). Luxembourg, as all of EU, will switch to daylight saving time during the night between Sat 27 March and Sun 28 March.
On Sat 27 March, Luxembourg time is CET (Central European Time, GMT+1).
On Sun 28 March, Luxembourg time is CEST (Central European Summer Time, GMT+2).
All the workshops will take place as virtual events. You will find below some tentative information about each workshop. For additional information, click over the workshop name in the schedule below or contact the workshop organizers.
WORKSHOP |
DATE |
Organizers |
| HCVS 2021 | Sunday, March 28 | This email address is being protected from spambots. You need JavaScript enabled to view it., This email address is being protected from spambots. You need JavaScript enabled to view it., This email address is being protected from spambots. You need JavaScript enabled to view it. |
| IFIP WG 1.3 meeting | Saturday & Sunday, March 27-28 (9.30 to 18.00, both days, by invitation only) | This email address is being protected from spambots. You need JavaScript enabled to view it. |
| LiVe 2021 | Saturday, March 27 | This email address is being protected from spambots. You need JavaScript enabled to view it. |
| QAVS 2021 | Friday, March 26 | This email address is being protected from spambots. You need JavaScript enabled to view it. and This email address is being protected from spambots. You need JavaScript enabled to view it. |
| Rust Verify (RW 2021) | April 7, 9 and 12 (online from 16h00 to 18h10 GMT) | This email address is being protected from spambots. You need JavaScript enabled to view it., This email address is being protected from spambots. You need JavaScript enabled to view it., This email address is being protected from spambots. You need JavaScript enabled to view it. |
| TADM 2021 | Saturday & Sunday, March 27-28 (afternoon, both days) | This email address is being protected from spambots. You need JavaScript enabled to view it. and This email address is being protected from spambots. You need JavaScript enabled to view it. |
| VerifyThis 2021 | Friday & Saturday, March 26-27 | This email address is being protected from spambots. You need JavaScript enabled to view it., This email address is being protected from spambots. You need JavaScript enabled to view it., This email address is being protected from spambots. You need JavaScript enabled to view it., This email address is being protected from spambots. You need JavaScript enabled to view it., This email address is being protected from spambots. You need JavaScript enabled to view it., This email address is being protected from spambots. You need JavaScript enabled to view it. |
| VPT 2021 | Saturday & Sunday, March 27-28 | This email address is being protected from spambots. You need JavaScript enabled to view it.and This email address is being protected from spambots. You need JavaScript enabled to view it. |
| FMSRL 2021 | TBA | This email address is being protected from spambots. You need JavaScript enabled to view it., This email address is being protected from spambots. You need JavaScript enabled to view it., This email address is being protected from spambots. You need JavaScript enabled to view it. |
8th Workshop on Horn Clauses for Verification and Synthesis (HCVS 2021)
Most Program Verification and Synthesis problems of interest can be modeled directly using Horn clauses and many recent advances in the Automated Deduction, Constraint/Logic Programming and Verification communities have centered around efficiently solving problems presented as Horn clauses.
This workshop aims to bring together researchers working in the communities of Automated Deduction (e.g CADE), Constraint/Logic Programming (e.g., ICLP and CP) and Program Verification community (e.g., CAV, TACAS, and VMCAI) on the topic of Horn clause based analysis, verification and synthesis.
Horn clauses for verification and synthesis have been advocated by these communities in different times and from different perspectives and this workshop is organized to stimulate interaction and a fruitful exchange and integration of experiences.
Workshop: Sunday, March 28, 2021
Website & Program: https://www.sci.unich.it/hcvs21/
For further details, contact the main organisers: This email address is being protected from spambots. You need JavaScript enabled to view it., This email address is being protected from spambots. You need JavaScript enabled to view it., This email address is being protected from spambots. You need JavaScript enabled to view it.
Submission: January 31, 2021
Notification: February 26, 2021
Camera-ready: March 13, 2021
IFIP Working Group 1.3 meeting 2021 Foundations of System Specifications (IFIP-WG-1.3 2021)
Aims: To support and promote the systematic development of the fundamental mathematical theory of systems specification. To investigate the theory of formal models for systems specification, development, transformation and verification.
Scope: The theoretical aspects of the specification and development of computing systems that are based on algebraic and logical concepts, and can be studied systematically within a theory of systems specification.
Remarks: This event is an on invitation only. It is a scientific workshop for the members of the IFIP WG 1.3 Foundations of System Specification.
Workshop: Saturday & Sunday, March 27-28, 2021 (9.30 - 18.00 both days)
Website: http://ifipwg13.cs.ovgu.de/
For further details, contact the main organiser: This email address is being protected from spambots. You need JavaScript enabled to view it.
5th Workshop on Learning in Verification (LiVe 2021)
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 general topic of machine learning in verification includes, for instance,
- the use of learning techniques (e.g. reinforcement learning) for speeding up verification (e.g. rigorous analysis of complex systems combining non-determinism, stochasticity, timing etc.),
- the use of machine learning data structures and algorithms (e.g. decision trees) for enhancing results of verification (e.g. generating simple invariants of programs generating small controllers of systems),
- verification of machine-learning artefacts (e.g. verification of neural networks), or
- meta-usage of machine learning (e.g. to predict the best tools to be applied to a verification problem).
Workshop: Saturday, March 27, 2021
Website & Program: https://www7.in.tum.de/~kretinsk/LiVe/2021
For further details, contact the main organiser: This email address is being protected from spambots. You need JavaScript enabled to view it.
Submission: February 1, 2021
Notification: March 1, 2021
Camera-ready: March 10, 2021
Second Workshop on Quantitative Aspects of Variant-rich Systems (QAVS 2021)
System variants often arise by configuring parameters that have a direct impact on the system’s behavior. Most prominently, in feature-oriented system design, features describe optional or incremental system functionalities whose configuration is simply whether a feature is active or inactive. Since the configuration space usually suffers from an exponential blowup in the number of configuration parameters, such variant-rich systems require specialized methods for their design, implementation, and analysis. Quantitative aspects such as probability of failure, energy consumption, or also numerical parameter values gain more and more attention due to the rising impact of co-adaptive and autonomous cyber-physical systems. While there are well-developed methodologies for variant-rich systems that do not take quantitative specifications into account, research on quantitative aspects is still done in fairly isolated branches. The main goal of this workshop is to bring researchers of the field together and foster their collaboration, presenting the different approaches to deal with non-functional properties of variant-rich systems.
Workshop: Friday, March 26, 2021
Website & Program: https://qavs.edgecloud.de
For further details, contact the main organisers: This email address is being protected from spambots. You need JavaScript enabled to view it. and This email address is being protected from spambots. You need JavaScript enabled to view it.
Submission: March 1st, 2021
Notification: March 14, 2021
Camera-ready: April 28, 2021
Rust Verify (RW2021)
Rust is a new programming language that is becoming increasingly popular for writing systems code. This workshop aims to bring together language designers, application developers and formal verification tool builders, to foster a community of those interested in developing verified Rust programs.
Workshop: April 7, 9 and 12, 2021 (online from 16h00 to 18h10 GMT)
Website & Program: https://sites.google.com/view/rustverify2021
For further details, contact the main organisers: This email address is being protected from spambots. You need JavaScript enabled to view it., This email address is being protected from spambots. You need JavaScript enabled to view it., This email address is being protected from spambots. You need JavaScript enabled to view it.
Submission: January 8, 2021
Notification: January 29, 2021
Camera-ready copy: March 28, 2021
First International Workshop on Trusted Automated Decision Making (TADM 2021)
When can automated decision-making systems be trusted? What is required for sufficient fairness, accountability and transparency? Decision-making logic of “black box” models such as deep neural networks cannot be comprehended by humans. Planning for trustworthy automation and its positive impact on life requires human and machine meta-cognition. What disciplines can help software professionals demonstrate trust in automated decision-making systems, especially those based on Machine Learning (ML)? Do adjunct models with "explainable AI" create a decision-making process that’s trustworthy enough? Should decisions impacting human safety be restricted to interpretable models? We invite transdisciplinary researchers, computer scientists, and practitioners whose research -- however nascent or recent – will initiate discussion. We particularly encourage research in-progress or of a speculative nature.
Workshop: Saturday and Sunday, March 27-28, 2021 (afternoon, both days)
Website & Program: https://3drationality.com/TADM2021/
For further details, contact the main organisers: This email address is being protected from spambots. You need JavaScript enabled to view it. and This email address is being protected from spambots. You need JavaScript enabled to view it.
Submission: January 22, 2021
Notification: February 19, 2021
Camera-ready: March 5, 2021
VerifyThis Verification Competition 2020 (VerifyThis 2021)
VerifyThis is a series of program verification competitions held earlier at FoVeOOS2011, FM2012, Dagstuhl (April 2014), ETAPS 2015-2019. 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.
Workshop/Competition: Friday and Saturday, March 26-27, 2021
Website & Program: https://www.pm.inf.ethz.ch/research/verifythis.html
For further details, contact the main organisers: This email address is being protected from spambots. You need JavaScript enabled to view it., This email address is being protected from spambots. You need JavaScript enabled to view it., This email address is being protected from spambots. You need JavaScript enabled to view it., This email address is being protected from spambots. You need JavaScript enabled to view it., This email address is being protected from spambots. You need JavaScript enabled to view it., This email address is being protected from spambots. You need JavaScript enabled to view it.
Register at: https://www.pm.inf.ethz.ch/research/verifythis/Participation.html
Registration/grant application deadline: March 13, 2021
9th International Workshop on Verification and Program Transformation (VPT 2021)
The aim of the workshop is to bring together researchers working in the fields of Program Verification and Program Transformation. There is great potential for beneficial interactions between these two fields because:
(i) methods and tools developed in the field of Program Transformation such as partial evaluation, fold/unfold transformations, and supercompilation, have all been applied with success in the field of the verification of infinite-state systems and parameterized systems, and
(ii) model checking, abstract interpretation, SAT and SMT solving and automated theorem proving have been used to enhance program transformation techniques. Moreover, the formal certification of program transformation tools, such as refactoring tools and compilers, has recently attracted considerable interest and posed major challenges.
Workshop: Saturday and Sunday, March 27-28, 2021
Website & Program: http://refal.botik.ru/vpt/vpt2021/
For further details, contact the main organisers: This email address is being protected from spambots. You need JavaScript enabled to view it.and This email address is being protected from spambots. You need JavaScript enabled to view it.
Submission: December 20, 2020
Notification: February 9, 2021
Camera-ready: February 22 2021
First Workshop on Formal Methods for Safe Reinforcement Learning (FMSRL)
As deep learning moves from the lab into real-world applications, ensuring the correctness and robustness of deep neural networks becomes a paramount concern. Specifying what it means for a neural network to behave correctly is a challenging problem, especially for classifiers and generative models. Verifying that deep networks meet these specifications is computationally challenging. Recent demonstrations of brittleness in deep learning – including adversarial examples and RL agents that learn pathological control policies – have motivated new computationally tractable approaches toward both specifying and verifying salient properties of neural networks. This workshop will bring together academics, industry researchers, and practitioners to delve into the current state of safe learning. Relevant topics include robustness evaluation/verification, safe reinforcement learning, fairness, robustness against model compression, interpretability, and deep learning with invariance and equivariance constraints.
Website: http://workshop.safelearning.ai
For further details, contact the main organisers: This email address is being protected from spambots. You need JavaScript enabled to view it., This email address is being protected from spambots. You need JavaScript enabled to view it., This email address is being protected from spambots. You need JavaScript enabled to view it.