Tutorial
Research Paper
Invited Talk

Times are depicted in China Standard Time (CST)

  Time  Title
Day 1
Saturday 20th - Sunday 21st November 2021
Session 1: 16:00 - 17:30

Tutorials:

tutorial 1: FMI Co-simulation Based Digital Twin (Peter Gorm Larsen, Hao Feng, Michael Sandberg)

tutorial 2: Momba

17:30 - 18:00 Break
Session 2: 18:00 - 19:30

Tutorials:

tutorial 1: FMI Co-simulation Based Digital Twin (Peter Gorm Larsen, Hao Feng, Michael Sandberg)

tutorial 2: Momba

19:30 - 20:00 Break
Session 3: 20:00 - 21:30

Tutorials:

tutorial 1: FMI Co-simulation Based Digital Twin (Simon Thrane Hansen, Frederik Palludan Madsen)

tutorial 3: Continuous Verification using CBMC (Michael Tautschnig)

21:30 - 22:00 Break
Session 4: 22:00 - 23:00

Tutorials:

tutorial 1: FMI Co-simulation Based Digital Twin (Mirgita Frasheri, Hugo Daniel Macedo, Ken Pierce, Cláudio Gomes)

tutorial 3: Continuous Verification using CBMC (Michael Tautschnig)

23:00 - 23:30 Break
Session 5: 23:30 - 0:30
0:30 - 1:00 Break
Session 6: 1:00 - 2:00
Day 2
Sunday 21st - Monday 22nd November 2021
Session 1: 16:00 - 17:30

Tutorials:

tutorial 4:FMTea

tutorial 5: Implementing an IDE for "tiny" Event-B with JetBrains Metaprogramming System MPS

17:30 - 18:00 Break
Session 2: 18:00 - 19:30

Tutorials:

tutorial 4:FMTea

tutorial 5: Implementing an IDE for "tiny" Event-B with JetBrains Metaprogramming System MPS

19:30 - 20:00 Break
Session 3: 20:00 - 21:30

Tutorials:

tutorial 4:FMTea

tutorial 5: Implementing an IDE for "tiny" Event-B with JetBrains Metaprogramming System MPS (Mikhail Barash)

21:30 - 22:00 Break
Session 4: 22:00 - 23:00

Tutorials:

tutorial 4:FMTea

tutorial 5: Implementing an IDE for "tiny" Event-B with JetBrains Metaprogramming System MPS  (Mikhail Barash)

23:00 - 23:30 Break
Session 5: 23:30 - 0:30
0:30 - 1:00 Break
Session 6: 1:00 - 2:00
Day 3
Monday 22nd - Tuesday 23rd November 2021
Session 1: 16:00 - 17:30 OPENING

Matt Griffin and Brijesh Dongol

Verifying Secure Speculation in Isabelle/HOL

Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin and Philippa Gardner

Two mechanisations of WebAssembly 1.0

17:30 - 18:00 Break
Session 2: 18:00 - 19:30 Franck Cassez

Verification of the Incremental Merkle Tree Algorithm with Dafny

Felix A. Wolf, Malte Schwerhoff and Peter Müller

Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDA

Adel Djoudi, Martin Hana and Nikolai Kosmatov

Formal verification of a JavaCard virtual machine with Frama-C

19:30 - 20:00 Break
Session 3: 20:00 - 21:30 Federico Mora, Murphy Berzish, Mitja Kulczynski, Dirk Nowotka and Vijay Ganesh

Z3str4: A Multi-armed String Solver

21:30 - 22:00 Break
Session 4: 22:00 - 23:00 Clark Barrett, joint with memocode

Invited Talk: Domain-Specific Reasoning with Satisfiability Modulo Theories

23:00 - 23:30 Break
Session 5: 23:30 - 0:30
0:30 - 1:00 Break
Session 6: 1:00 - 2:00
Day 4
Tuesday 23rd - Wednesday 24th November 2021
Session 1: 16:00 - 17:30 Paula Herber

Invited Talk: Combine Forces - How to Formally Verify Informally Defined Embedded Systems

17:30 - 18:00 Break
Session 2: 18:00 - 19:30 Gal Amram, Shahar Maoz, Or Pistiner and Jan Oliver Ringert

Efficient Algorithms for ω-Regular Energy Games

Krishna SKhushraj MadnaniManuel Mazo Jr. and Paritosh Pandya

Generalizing Non-Punctuality for Timed Temporal Logic with Freeze Quantifiers

Matias Scharager, Katherine Cordwell, Stefan Mitsch and André Platzer

Verified Quadratic Virtual Substitution for Real Arithmetic

19:30 - 20:00 Break
Session 3: 20:00 - 21:30 Rim Saddem-Yagoubi, Pascal Poizat and Sara Houhou

Business Processes Meet Spatial Concerns: the sBPMN Verification Framework

Mark BattyBrijesh Dongol and Daniel Wright

Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies

Jinting Bian, Hans-Dieter Hiep, Frank De Boer and Stijn De Gouw

Integrating ADTs in KeY and their Application to History-based Reasoning

21:30 - 22:00 Break
Session 4: 22:00 - 23:00 Alexandra Bugariu, Arshavir Ter-Gabrielyan and Peter Müller

Identifying Overly Restrictive Matching Patterns in SMT-based Program Verifiers

Nicholas Coughlin, Kirsten Winter and Graeme Smith

Rely/guarantee reasoning for multicopy atomic weak memory models

23:00 - 23:30 Break
Session 5: 23:30 - 0:30
0:30 - 1:00 Break
Session 6: 1:00 - 2:00
Day 5
Wednesday 24th - Thursday 25th November 2021
Session 1: 16:00 - 17:30 FME Fellow
17:30 - 18:00 Break
Session 2: 18:00 - 19:30 Sota Sato, Atsuyoshi Saimen, Masaki Waga, Kenji Takao and Ichiro Hasuo

Hybrid System Falsification for Multiple-Constraint Parameter Synthesis: a Gas Turbine Case Study

Zhenya Zhang and Paolo Arcaini

Gaussian Process-Based Confidence Estimation for Hybrid System Falsification

Julius AdeltTimm Liebrenz and Paula Herber

Formal Verification of Intelligent Hybrid Systems that are modeled with Simulink and the Reinforcement Learning Toolbox

19:30 - 20:00 Break
Session 3: 20:00 - 21:30 Simon Foster, Mario Gleirscher, Jonathan Huerta Y Munive and Georg Struth

Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs

Bing Sun, Jun Sun, Ting Dai and Lijun Zhang

Probabilistic Verification of Neural Networks Against Group Fairness

Joseph Scott, Hammad Rehman, Trishal Sudula, Federico Mora and Vijay Ganesh

BanditFuzz: Fuzzing SMT Solvers with Multi-Agent Reinforcement Learning

21:30 - 22:00 Break
Session 4: 22:00 - 23:00 Alexei Kopylov, Stefan Mitsch, Aleksey Nogin and Michael Warren

Formally Verified Safety Net for Waypoint Navigation Neural Network Controllers

Ernst Moritz Hahn, Mateo Perez, Sven ScheweFabio SomenziAshutosh Trivedi and Dominik Wojtczak

Model-Free Reinforcement Learning for Lexicographic Omega-Regular Objectives

23:00 - 23:30 Break
Session 5: 23:30 - 0:30
0:30 - 1:00 Break
Session 6: 1:00 - 2:00
Day 6
Thursday 25th - Friday 26th November 2021
Session 1: 16:00 - 17:30 Assia Mahboubi

Invited Talk: Formal verification of computational mathematics

17:30 - 18:00 Break
Session 2: 18:00 - 19:30 Yong LiYih-Kuen TsayAndrea TurriniMoshe Vardi and Lijun Zhang

Congruence Relations for B\"uchi Automata

Maurice ter BeekGuillermina CledouRolf Hennicker and José Proença

Featured Team Automata

Anastasia Mavridou, Andreas Katis, Dimitra Giannakopoulou, David Kooi, Thomas Pressburger and Michael W. Whalen

From Partial to Global Assume-Guarantee Contracts: Compositional Realizability Analysis in FRET

19:30 - 20:00 Break
Session 3: 20:00 - 21:30 Andrea Pferscher and Bernhard K. Aichernig

Fingerprinting Bluetooth Low Energy Devices via Active Automata Learning 

21:30 - 22:00 Break
Session 4: 22:00 - 23:00
23:00 - 23:30 Break
Session 5: 23:30 - 0:30
0:30 - 1:00 Break
Session 6: 1:00 - 2:00
Day 7
Friday 26th - Saturday 27th November 2021
Session 1: 16:00 - 17:30 Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotný, Jiří Zárevúcky and Djordje Zikelic

On Lexicographic Proof Rules for Probabilistic Termination

František Blahoudek, Murat CubuktepePetr NovotnýMelkior OrnikPranay Thangeda and Ufuk Topcu

Fuel in Markov Decision Processes (FiMDP): A Practical Approach to Consumption

Oyendrila Dobe, Erika AbrahamEzio Bartocci and Borzoo Bonakdarpour

HyperProb: A Model Checker for Probabilistic Hyperproperties (short)

Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen and Laura Kovács

The Probabilistic Termination Tool Amber (short)

17:30 - 18:00 Break
Session 2: 18:00 - 19:30 Weijiang Hong, Zhenbang Chen, Yide Du and Ji Wang

Trace Abstraction-based Verification for Uninterpreted Programs

Felipe Gorostiaga and Cesar Sanchez

HStriver: a Very Functional Extensible Tool for the Runtime Verification of Real-Time Event Streams

Rong Gu, Cristina Seceleanu, Eduard Enoiu and Kristina Lundqvist

Model Checking Collision Avoidance of Nonlinear Autonomous Vehicle Models

19:30 - 20:00 Break
Session 3: 20:00 - 21:30 Cui Su and Jun Pang

CABEAN 2.0: Efficient and Efficacious Control of Asynchronous Boolean Networks

Ionut Tutu, Claudia Chirita and José Luiz Fiadeiro

Dynamic Reconfiguration via Typed Modalities

21:30 - 22:00 Break
Session 4: 22:00 - 23:00 Mingsheng Ying

Invited Talk: Model Checking for Verification of Quantum Circuits

23:00 - 23:30 Break
Session 5: 23:30 - 0:30 Closing of the conference
0:30 - 1:00 Break
Session 6: 1:00 - 2:00