Accepted papers

The following papers have been accepted at SEFM 2024. The indicated artifact badges follow the EAPLS badging scheme.

Authors	Title	Badges
Kangfeng Ye, Roberto Metere, Poonam Yadav	User-Guided Verification of Security Protocols via Sound Animation
Margherita Renieri, Letterio Galletta	A Policy Framework for Regulating External Calls in Smart Contracts
Alessandro Cimatti, Thomas Møller Grosen, Kim Guldstrand Larsen, Stefano Tonetta, Martin Zimmermann	Exploiting Assumptions for Effective Monitoring of Real-Time Properties under Partial Observability
Adele Veschetti, Richard Bubel, Reiner Hähnle	SmartML: Towards a Modeling Language for Smart Contracts
Jonas Becker-Kupczok, Paula Herber	Symbolic Execution for Precise Information Flow Analysis of Timed Concurrent Systems
Horatiu Cirstea, Markus A. Kuppe, Benjamin Loillier, Stephan Merz	Validating Traces of Distributed Programs Against TLA+ Specifications
Narges Khakpour, David Parker	Partially-Observable Security Games for Automating Attack-Defense Analysis
Diego Marmsoler, Asad Ahmed, Achim D. Brucker	Secure Smart Contracts with Isabelle/Solidity
Ellen Wittingen, Marieke Huisman, Ömer Şakar	Deductive verification of SYCL in VerCors
Jan Tušil, Jan Obdrzalek	Minuska: Towards a Formally Verified Programming Language Framework
Benjamin von Berg, Bernhard Aichernig, Maximilian Rindler, Darko Stern, Martin Tappler	Hierarchical Learning of Generative Automaton Models from Sequential Data
Salman Farhat, Simon Bliudze, Laurence Duchien, Olga Kouchnarenko	Composing Run-time Variability Models
Raúl Pardo, Daniel Le Métayer	Model-Checking the Implementation of Consent
Hannes Sochor, Flavio Ferrarotti, Robert Wille	GrammarForge: Learning Program Input Grammars for Fuzz Testing
Adam Petz, Will Thomas, Anna Fritz, Tj Barclay, Logan Schmalz, Perry Alexander	Verified Configuration and Deployment of Layered Attestation Managers
Ana Jovanovic, Allison Sullivan	Right or Wrong – Understanding How Users Write Software Models in Alloy
Vasileios Koutavas, Yu-Yang Lin, Nikos Tzevelekos	An Operational Semantics for Yul
Étienne André, Marie Duflot, Laetitia Laversa, Engel Lefaucheux	Execution-time opacity control for timed automata
Siddharth Priya, Temesghen Kahsai, Arie Gurfinkel	Unlocking the Power of Environment Assumptions for Unit Proofs
Ivan Lanese, Ugo Dal Lago, Vikraman Choudhury	Towards Quantum Multiparty Session Types
Philip Tasche, Paula Herber, Marieke Huisman	Automated Invariant Generation for Efficient Deductive Reasoning about Embedded Systems
Matteo Paier, Roberto Van Eeden, Marino Miculan	Formal Analysis of Multi-Factor Authentication Schemes in Digital Identity Cards
Srajan Goyal, Alberto Griggio, Stefano Tonetta	Leveraging Contracts for Failure Monitoring and Identification in Automated Driving Systems