Programme – Satellite Events

Programme of satellite events during the weekend.

LiVe RRRR TADM ASQAP EMW FMBC PLACES TLA VSS

9th Workshop on Learning in Verification (Saturday)

Saturday, May 3, Room: MDCL 1016

Programme to be announced

4rd Workshop on Reproducibility and Replication of Research Results (Saturday)

Saturday, May 3, Room: MDCL 1008

Programme to be announced

International Workshop on Trusted Automated Decision-Making (Saturday)

Saturday, May 3, Room: MDCL 1110

Programme to be announced

First International Workshop on Autonomous System Quality Assurance and Prediction with Digital Twins (Sunday)

Sunday, May 4, Room: MDCL 1008

9:00–9:05

Welcome + Coffee

9:05–10:00

GM technologies overview and examples of DT use in the automotive industry

Mehrnoosh Askarpour

10:00–10:30

Coffee Break

10:30–10:50

Co-Development of Physical and Digital Twins: Augmenting Capabilities and Increasing Fault Tolerance

Irina Muntean, Mirgita Frasheri and Tiziano Munaro

10:50–11:10

BedreFlyt: Improving Patient Flows through Hospital Wards with Digital Twins

Riccardo Sieve, Paul Kobialka, Laura Slaughter, Rudolf Schlatte, Einar Broch Johnsen and Silvia Lizeth Tapia Tarifa

11:10–11:30

Verification of Digital Twins using Classical & Statistical Model Checking

Raghavendran Gunasekaran and Boudewijn Haverkort

11:30–12:30

DTaaS Tool Demo

TBA

ETAPS Mentoring Workshop (Sunday)

Sunday, May 4, Room: MDCL 1016

8:25–8:30

Welcome

Marc Frappier

8:30–9:15

Things Rarely Talked About in Academia: Failures and Management

Ina Schaefer

9:15–10:00

Descriptive and prescriptive models in formal system developments

Yamine Ait Ameur

10:00–10:30

coffe break

10:30–11:15

My Humble Journey Through Academia

Michael Blondin

11:15–12:00

How to Fit it All In

Marsha Chechik

12:00–12:30

Free discussions with speakers

12:30–14:00

lunch

14:00–14:45

From Recursive Domain Equations to Reinforcement Learning for COVID

Kim Guldstrand Larsen

14:45–15:30

Building Resilience for a Research Career

Eunsuk Kang

15:30–16:00

Free discussions with speakers

16:00–16:30

coffee break

16:30–17:15

A Formal Methods Fellowship

Marie Farrell

6th International Workshop on Formal Methods for Blockchains (Sunday)

Sunday, May 4, Room: MDCL 1110

9:00–9:05

Welcome

Diego Marmsoler, Meng Xu

9:05–10:00

Bringing the Power of Interactive Theorem Proving to Web3

Julian Sutherland

10:00–10:30

Coffee Break

10:30–10:55

Formal Specification of Smart Contracts via Bisimulation in Coq

Derek Sorensen

10:55–11:20

Verifying Smart Contract Transformations Using Bisimulations

Kegan McIlwaine, James Caldwell

11:20–11:40

Isabell/Solidity: A tool for the Verification of Solidity Smart Contracts

Asad Ahmed, Diego Marmsoler

11:40–12:05

Formal verification in Solidity and Move: insights from a comparative analysis

Massimo Bartoletti, Silvia Crafa, Enrico Lipparini

12:05–12:30

Validity, Liquidity, and Fidelity: Formal Verification for Smart Contracts in Cardano

Tudor Ferariu, Philip Wadler, Orestis Melkonian

12:30–13:35

Lunch Break

13:35–14:30

Is Formal Verification Practical?

Wolfgang Grieskamp

14:30–15:00

Coffee Break

15:00–15:25

Program logics for ledgers

Orestis Melkonian, Wouter Swierstra, James Chapman

15:25–15:50

Formal Verification of a Fail-Safe Cross-Chain Bridge

Filip Maric, Bernhard Scholz, Pavle Subotić

15:50–16:15

A Readable and Computable Formalization of the Streamlet Consensus Protocol

Mauro Jaskelioff, Orestis Melkonian, James Chapman

16:15–16:40

Towards a Mechanization of Fraud Proof Games in Lean

Martin Ceresa, Cesar Sanchez

16:40–17:00

Coffee Break

17:00–17:25

ByteSpector: A Verifying Disassembler for EVM Bytecode

Franck Cassez

17:25–17:50

SCAR: Verification-based Development of Smart Contracts

Jonas Schiffl, Bernhard Beckert

17:50–18:10

A Benchmark Framework for Byzantine Fault Tolerance Testing Algorithms

João Miguel, Louro Neto, Burcu Kulahcioglu Ozkan

18:10–18:25

Closing

Diego Marmsoler, Meng Xu

Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software (Sunday)

Sunday, May 4, Room: MDCL 1116

9:05–10:00

TBA

Giovanni Bernardi

10:00–10:30

Coffee Break

10:30–11:00

Thread and Memory Safe Programming with CLASS

Luis Caires

11:00–11:30

Type Congruence, Duality and Iso-Recursive Binary Session Types

Marco Giunti and Nobuko Yoshida

11:30–12:00

Local Type Inference for Context-Free Session Types

Bernardo Almeida, Andreia Mordido and Vasco T. Vasconcelos

12:00–12:30

Capturing Happens-Before in Types

Grant Iraci, Michael Piskozub, Frank Tsai, Lukasz Ziarek and Andrew Hirsch

12:30–14:00

Lunch

14:00–14:30

AMP: Automata-based Multiparty Protocols Framework

Felix Stutz and Emanuele D'Osualdo

14:30–15:00

Separation and Encodability in Mixed Choice Multiparty Sessions

Nobuko Yoshida

15:00–15:30

Choreographies as Macros

Alexander Bohosian and Andrew K. Hirsch

15:30–16:00

An Efficient Implementation of Guard-Based Synchronization for an Object-Oriented Programming Language

Shucai Yao and Emil Sekerinski

16:00–16:30

Coffee Break

16:30–17:00

Static Communication Analysis for Hardware Design

Mads Rosendahl and Maja Hanne Kirkeby

TLA+ Community Event (Sunday)

Sunday, May 4, Room: MDCL-1115

9:00–9:45

Formal models for monotonic pipeline architectures

J.-P. Bodeveix, A. Bonenfant, T. Carle, M. Filali, C. Rochange

9:45–10:30

ModelFuzz: Model guided fuzzing of distributed systems

S. Nagendra

10:30–10:45

Coffee Break

10:45–11:30

Translating C to PlusCal for Model Checking of Safety Properties on Source Code

G. di Fatta, E. Ohayon, A. Methni

11:30–12:00

TLA+ for All: Model Checking in a Python Notebook

K. Läufer, G.K. Thiruvathukal

12:00–13:00

Lunch

13:00–13:45

TLA+ Modeling of MongoDB Transactions

M. Demirbas, W. Schultz

13:45–14:30

Automating Trace Validation with PGo

F. Hackett, I. Beschastnikh

14:30–14:45

Coffee Break

14:45–15:15

It's never been easier to write TLA+ tooling!

A. Helwer

15:15–15:45

Are We Serious About Using TLA+ For Statistical Properties?

A. Jesse Jiryu Davis

15:45–16:15

Discussion Panel

International Workshop on Verification of Scientific Software (Sunday)

Sunday, May 4, Room: MDCL 1010

9:00–10:00

Foundational end-to-end verification of numerical programs (Keynote talk)

Andrew Appel

10:00–10:30

Coffee

10:30–11:00

Towards Richer Challenge Problems for Scientific Computing Correctness

Matthew Sottile, Mohit Tekriwal, and John Sarracino

11:00–11:30

Verifying a Sparse Matrix Algorithm Using Symbolic Execution

Alex Wilton

11:30–12:00

Mechanizing Olver’s Error Arithmetic

Max Fan, Ariel E. Kellison, and Samuel D. Pollard

12:00–12:30

Property Testing for Ocean Models. Can We Specify It?

Deepak Cherian

12:30–14:00

Lunch

14:00–14:45

Automated Program Analysis for Scientific Software (Keynote talk)

Jacob Laurel

14:45–15:15

Fast Trigonometric Functions using the RLIBM Approach

Sehyeok Park and Santosh Nagarakatte

15:15–15:45

Specification and Verification for Climate Modeling: Formalization Leading to Impactful Tooling

Alper Altuntas, Allison H. Baker, Ganesh Gopalakrishnan, John Baugh, and Stephen Siegel

15:45–16:00

Introduction to Challenge Problems

Stephen Siegel

16:00–16:30

Coffee

16:30–17:00

Challenge Problem Presentations

various

Main Programme