Programme

All times are listed for CET+1 (Central European Summer Time)

Monday 15 June

Tutorials

Time Distributed Computing Track Verification Track
10.30-12.00 Choreographic Development of Message-Passing Applications Parameterized Verification with Byzantine Model Checker
12.00-13.30 break break
13.30-15.00 CHOReVOLUTION IDRE: An Integrated Development and Run-time Environment for Automatically Realizing and Executing Distributed Applications The Probabilistic Model Checker Storm
15.00-15.30 break break
15.30-17.00 Kollaps/Thunderstorm: Reproducible Evaluation of Distributed Systems Typechecking Java protocols with Mungo/StMungo


Tuesday 16 June

Invited Talk

10.00-11.00:     Peter Kriens   Formal Specifications to Increase Understanding

Conference Talks

Time COORDINATION DAIS FORTE
11.00-11.30 break break break
11.30-12.00 Operational representation of dependencies in Context-Dependent Event Structures On the trade-offs of combining multiple secure processing primitives for data analytics  
12.00-12.30 Architecture modelling of parametric component-based systems Capturing Privacy-preserving User Contexts with IndoorHash  
12.30-14.00 break break break
14.00-14.30 Weighted PCL over product valuation monoids Self-Tunable DBMS Replication with Reinforcement Learning  
14.30-15.00 A Choreography-Driven Approach to APIs: the OpenDXL Case Study A microservice architecture to automate the evaluation of Android machine learning detection systems  
15.00-15.30 break break break
15.30-16.00 Choreography Automata    
16.00-16.20 Team Automata@Work: On Safe Communication    
16.20-16.40 Event-based Non-intrusive Customization of Multi-tenant SaaS Using Microservices    
16.40-17.00 Quality of Service ranking by quantifying partial compliance of requirements    


Wednesday 17 June

Invited Talk

10.00-11.00:     Nathalie Bertrand   Probabilistic Threshold Automata for Modeling and Verifying Randomized Distributed Algorithms

Conference Talks

Time COORDINATION DAIS FORTE
11.00-11.30 break break break
11.30-12.00 A true concurrent model of smart contracts executions    
12.00-12.30   TailX: Scheduling Heterogeneous Multiget Queries to Improve Tail Latencies in Key-Value Stores  
12.30-13.00     Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory
13.00-14.00 break break break
14.00-14.30 GoPi: Compiling linear and static channels in Go Towards hypervisor support for enhancing the performance of virtual machine introspection Derivation of Heard-Of Predicates From Elementary Behavioral Patterns
14.30-15.00 SFJ: An Implementation of Semantic Featherweight Java Fed-DIC: Diagonally Interleaved Coding in a Federated Cloud Environment Trace Equivalence and Epistemic Logic to Express Security Properties
15.00-15.30 break break break
15.30-16.00 Implementation of Multiparty Session Types in Rust
(10 min break at 15:50)
Towards a Polyglot Data Access Layer for a Low-Code Application Development Platform A Formal Framework for Consent Management
16.00-16.30 Renegotiation and recursion in Bitcoin contract A Comparison of Message Exchange Patterns in BFT Protocols Towards Bridging Time and Causal Reversibility
16.30-16.50 Towards a Formally Verified EVM in Production Environment    


Thursday 18 June

Invited Talk

10.00-11.00:     Holger Hermanns   Power-Optimal Scheduling of LEO Satellite Networks

Conference Talks

Time COORDINATION DAIS FORTE
11.00-11.30 break break break
11.30-12.00 Towards Energy-, Time- and Security-aware Multi-core Coordination A resource usage efficient distributed allocation algorithm for 5G Service Function Chains Conformance-Based Doping Detection for Cyber-Physical Systems
12.00-12.30 ARx: Reactive Programming for Synchronous Connectors A Stabilizing One-To-Many Node-Disjoint paths Routing Algorithm in Star Networks Strategy Synthesis for Autonomous Driving in a Moving Block Railway System with Uppaal Stratego
12.30-13.30 break break break
13.30-14.00 Time-fluid field-based coordination    
14.00-14.30 Resilient Distributed Collection through Information Speed Thresholds   Towards Deep Statistical Model Checking
14.30-15.00 Refined Mean Field Analysis: The Gossip Shuffle Protocol Revisited   Towards a Hybrid Verification Methodology for Communication Protocols
15.00-15.30 break break break
15.30-16.00 Formal Modeling and Analysis of Medical Systems   Probabilistic Timed Automata with One Clock and Initialised Clock-Dependent Probabilities
16.00-16.30 On Implementing Symbolic Controllability   On Implementable Timed Automata
16.30-17.00 Combining SLiVER with CADP to Analyze Multi-agent Systems    


Coordination accepted papers and programme

Coordination Best Paper

Modelling 1

(session chair: Chiara Bodei)

Modelling 2 / Message-based communication 1

(session chair: Roberto Guanciale)

Message-based communication 2 / Microservices

(session chair: Alberto Lluch Lafuente)

Communications: types & implementations

(session chair: Hugo Torres Vieira)

Digital contracts

(session chair: Anastasia Mavridou)

Coordination Languages

(session chair: Jean-Marie Jacquet)

Large Scale Decentralised Systems

(session chair: Michele Loreti)

Verification and Analysis

(session chair: Mieke Massink)

DAIS accepted papers and programme

DAIS Best Paper

Privacy and Security

(session chair: Sonia Ben Mokthar)

ML for Systems

(session chair: Vana Kalogeraki)

Cloud and Systems

(session chair: Valerio Schiavoni)

Fault-tolerance and Reproducibilty

(session chair: Hans Reiser)

Distributed Algorithms

(session chair: Anne Remke)

FORTE accepted papers and programme

FORTE Best Paper

Program Logics

(session chair: TBA)

Formal Frameworks

(session chair: TBA)

Verification 1

(session chair: TBA)

Verification 2

(session chair: TBA)

Timed Automata

(session chair: TBA)