FORCE — PROGRAM
Days: Saturday, 25 July 2026
Saturday, 25 July 2026
08:30-08:40
Introduction to workshop
FORCE
Location:
C2.01
08:40-10:25
Industrial applications
FORCE
Location:
C2.01
| 08:40-09:25 |
Compositional reasoning for defense and aerospace systems (abstract) 45 min
1 Collins Aerospace
|
| 09:25-09:45 |
Formal Specification and Verification for Trustworthy Automotive Embedded Systems: An Experience Report and Outlook (abstract) 20 min
1 KTH Royal Institute of Technology
2 TRATON AB, Sweden
|
| 09:45-10:05 |
Multimode System Design with CoSApp (abstract) 20 min
1 Safran
|
| 10:05-10:25 |
The ∆Q Systems Development Paradigm (abstract) 20 min
1 PLWorkz R&D
|
10:25-10:55
Coffee Break
FORCE
Location:
C2.01
10:55-12:15
Runtime monitoring
FORCE
Location:
C2.01
| 10:55-11:15 |
Compositional Conformal Certification for Reusable Vision-Based Runtime Monitoring (abstract) 20 min
1 Toyota Motor North America R&D
2 ETH Zurich
|
| 11:15-11:35 |
A Unified Framework for Runtime Verification and Model-Based Diagnosis in LOLA (abstract) 20 min
1 University of Luebeck
2 University of Klagenfurt
|
| 11:35-11:55 |
Lifting Pacti Contracts into MLTL and Runtime Monitors (abstract) 20 min
1 Iowa State University
|
| 11:55-12:15 |
Coherence Constraints as Compositional Contracts for Autonomic Systems (abstract) 20 min
1 SWEN, Università degli Studi dell’Aquila, L’Aquila, Italy
2 FMT Lab, CNR–ISTI, Pisa, Italy
|
12:15-13:30
Lunch
FORCE
Location:
C2.01
13:30-15:15
Autonomous and learning-enabled systems
FORCE
Location:
C2.01
| 13:30-14:15 |
Safe Autonomous Systems via Shielding (abstract) 45 min
1 Graz University of Technology
|
| 14:15-14:35 |
MTL for Compositional Specification of Assume Guarantee Contracts in Autonomous Robotics (abstract) 20 min
1 University of Manchester
|
| 14:35-14:55 |
A Formal Algorithmic Framework for Probabilistic Assurance Cases for Learning-Enabled Systems (abstract) 20 min
1 University of California, Santa Cruz
2 University of Michigan
3 University of California, Berkeley
|
| 14:55-15:15 |
Agentic Model Checking of LLM-Generated Systems Code (abstract) 20 min
1 MBZUAI
2 Amazon
|
15:15-15:45
Coffee Break
FORCE
Location:
C2.01
15:45-17:25
Theory and logics
FORCE
Location:
C2.01
| 15:45-16:05 |
Contract-Based Architecture Exploration for Efficient Cyber-Physical System Design (abstract) 20 min
1 UC Berkeley
|
| 16:05-16:25 |
Heterogeneous Dynamic Logic: Provability Modulo Program Theories (abstract) 20 min
1 Karlsruhe Institute of Technology (KIT)
|
| 16:25-16:45 |
Towards a computable and compositional semantics of hybrid systems (abstract) 20 min
1 Università di Padova
2 University of Maastricht
3 Università di Verona
|
| 16:45-17:05 |
Taming Big CATs (abstract) 20 min
1 TU Darmstadt
|
| 17:05-17:25 |
Compositional Design of Society-Critical Systems (abstract) 20 min
1 MIT
|
17:25-17:55
Discussion and conclusion
FORCE
Location:
C2.01