Formal Reasoning for Compositional Systems Engineering (FORCE)


CAV 2026 Workshop
July 25, 2026


Lisbon, Portugal

8:30 - 8:40

Introduction to workshop

Session: Industrial applications

8:40 - 9:25

Keynote: Compositional reasoning for defense and aerospace systems
Darren Cofer, Collins Aerospace

9:25 - 9:45

Formal Specification and Verification for Trustworthy Automotive Embedded Systems: An Experience Report and Outlook
Jesper Amilon, KTH Royal Institute of Technology
Gustav Ung, TRATON AB, Sweden
Merlijn Sevenhuijsen, TRATON AB, Sweden
Karl Palmskog, KTH Royal Institute of Technology
Dilian Gurov, KTH Royal Institute of Technology
Mattias Nyberg, TRATON AB, Sweden

9:45 - 10:05

Multimode System Design with CoSApp
Etienne Lac, Safran

10:05 - 10:25

The ∆Q Systems Development Paradigm
Seyed Hossein HAERI, PLWorkz R&D

10:25 - 10:55

Coffee break

Session: Runtime monitoring

10:55 - 11:15

Compositional Conformal Certification for Reusable Vision-Based Runtime Monitoring
Bardh Hoxha, Toyota Motor North America R&D
Oliver Schön, ETH Zurich
Hideki Okamoto, Toyota Motor North America R&D
Lars Lindemann, ETH Zurich
Georgios Fainekos, Toyota Motor North America R&D

11:15 - 11:35

A Unified Framework for Runtime Verification and Model-Based Diagnosis in LOLA
Raik Hipler, University of Luebeck
Martin Leucker, University of Luebeck
Patrick Rodler, University of Klagenfurt

11:35 - 11:55

Lifting Pacti Contracts into MLTL and Runtime Monitors
Michael Jacks, Iowa State University
Kristin Yvonne Rozier, Iowa State University

11:55 - 12:15

Coherence Constraints as Compositional Contracts for Autonomic Systems
Antonio Bucchiarone, SWEN, Università degli Studi dell’Aquila, L’Aquila, Italy
Maurice H. ter Beek, FMT Lab, CNR–ISTI, Pisa, Italy
Alfonso Pierantonio, SWEN, Università degli Studi dell’Aquila, L’Aquila, Italy

12:15 - 13:30

Lunch

Session: Autonomous and learning-enabled systems

13:30 - 14:15

Keynote: Safe Autonomous Systems via Shielding
Bettina Könighofer, Graz University of Technology

14:15 - 14:35

MTL for Compositional Specification of Assume Guarantee Contracts in Autonomous Robotics
Natalia Ślusarz, University of Manchester
Marie Farrell, University of Manchester
Michael Fisher, University of Manchester

14:35 - 14:55

A Formal Algorithmic Framework for Probabilistic Assurance Cases for Learning-Enabled Systems
Eric Vin, University of California, Santa Cruz
Kyle A. Miller, University of California, Santa Cruz
Inigo Incer, University of Michigan
Sanjit A. Seshia, University of California, Berkeley
Daniel J. Fremont, University of California, Santa Cruz

14:55 - 15:15

Agentic Model Checking of LLM-Generated Systems Code
Youcheng Sun, MBZUAI
Jiawen Liu, MBZUAI
Daniel Kroening, Amazon
Jason Xue, MBZUAI

15:15 - 15:45

Coffee break

Session: Theory and logics

15:45 - 16:05

Contract-Based Architecture Exploration for Efficient Cyber-Physical System Design
Yifeng Xiao, UC Berkeley
Pierluigi Nuzzo, UC Berkeley

16:05 - 16:25

Heterogeneous Dynamic Logic: Provability Modulo Program Theories
Samuel Teuber, Karlsruhe Institute of Technology (KIT)
Mattias Ulbrich, Karlsruhe Institute of Technology (KIT)
André Platzer, Karlsruhe Institute of Technology (KIT)
Bernhard Beckert, Karlsruhe Institute of Technology (KIT)

16:25 - 16:45

Towards a computable and compositional semantics of hybrid systems
Davide Bresolin, Università di Padova
Pieter Collins, University of Maastricht
Luca Geretti, Università di Verona
Roberto Segala, Università di Verona
Tiziano Villa, Università di Verona

16:45 - 17:05

Taming Big CATs
Marco Scaletta, TU Darmstadt

17:05 - 17:25

Compositional Design of Society-Critical Systems
Gioele Zardini, MIT

17:25 - 17:55

Discussion and conclusion