Program

Real-time (Session Chair: A. Knapp)

Exploiting Assumptions for Effective Monitoring of Real-Time Properties under Partial Observability
Alessandro Cimatti, Thomas Møller Grosen, Kim Guldstrand Larsen, Stefano Tonetta and Martin Zimmermann

Execution-time opacity control for timed automata
Étienne André, Marie Duflot, Laetitia Laversa and Engel Lefaucheux

Symbolic Execution for Precise Information Flow Analysis of Timed Concurrent Systems
Jonas Becker-Kupczok and Paula Herber

Security & Trust I (Session Chair: S. Merz)

Model-Checking the Implementation of Consent
Raúl Pardo and Daniel Le Métayer

Formal Analysis of Multi-Factor Authentication Schemes in Digital Identity Cards
Matteo Paier, Roberto Van Eeden and Marino Miculan

Partially-Observable Security Games for Attack-Defence Analysis in Software Systems
Narges Khakpour and David Parker

Testing & Learning (Session Chair: A. Cerone)

GrammarForge: Learning Program Input Grammars for Fuzz Testing
Hannes Sochor, Flavio Ferrarotti and Robert Wille

Unlocking the Power of Environment Assumptions for Unit Proofs
Siddharth Priya, Temesghen Kahsai and Arie Gurfinkel

Hierarchical Learning of Generative Automaton Models from Sequential Data
Benjamin von Berg, Bernhard Aichernig, Maximilian Rindler, Darko Stern and Martin Tappler

Contracts & Invariants (Session Chair: O. Kouchnarenko)

Validating Traces of Distributed Programs Against TLA+ Specifications
Horatiu Cirstea, Markus A. Kuppe, Benjamin Loillier and Stephan Merz

Leveraging Contracts for Failure Monitoring and Identification in Automated Driving Systems
Srajan Goyal, Alberto Griggio and Stefano Tonetta

Automated Invariant Generation for Efficient Deductive Reasoning about Embedded Systems
Philip Tasche, Paula Herber and Marieke Huisman

Security & Trust II (Session Chair: R. Pardo)

User-Guided Verification of Security Protocols via Sound Animation
Kangfeng Ye, Roberto Metere and Poonam Yadav

Verified Configuration and Deployment of Layered Attestation Managers
Adam Petz, Will Thomas, Anna Fritz, Tj Barclay, Logan Schmalz and Perry Alexander

Smart Contracts(Session Chair: A.Knapp)

A Policy Framework for Regulating External Calls in Smart Contracts
Margherita Renieri and Letterio Galletta

SmartML: Towards a Modeling Language for Smart Contracts
Adele Veschetti, Richard Bubel and Reiner Hähnle

Secure Smart Contracts with Isabelle/Solidity
Diego Marmsoler, Asad Ahmed and Achim D. Brucker

Semantics and Verification (Session Chair: Ivan Lanese)

An Operational Semantics for Yul
Vasileios Koutavas, Yu-Yang Lin and Nikos Tzevelekos

Deductive verification of SYCL in VerCors
Ellen Wittingen, Marieke Huisman and Ömer Şakar

Minuska: Towards a Formally Verified Programming Language Framework
Jan Tušil and Jan Obdrzalek

Specification (Session Chair: A. Madeira)

Towards Quantum Multiparty Session Types
Ivan Lanese, Ugo Dal Lago and Vikraman Choudhury

Right or Wrong -- Understanding How Users Write Software Models in Alloy
Ana Jovanovic and Allison Sullivan

Composing Run-time Variability Models
Salman Farhat, Simon Bliudze, Laurence Duchien and Olga Kouchnarenko