Colloquium on Design and Verification of Cyber-Physical Systems: From Theory to Applications
Organisers
Bernd Finkbeiner
CISPA Helmholtz Center for Information Security, Saarbrücken, DE
Andreas Rauh
Carl von Ossietzky Universität Oldenburg, DE
Paul Kröger
Carl von Ossietzky Universität Oldenburg, DE
Organisational contact
Kathrin Kuper
Carl von Ossietzky Universität Oldenburg
Venue
Carl von Ossietzky Universität Oldenburg
Campus Haarentor
Assembly hall, Building A11, Room 0-009
Ammerländer Heerstraße 69
26129 Oldenburg
Germany
Colloquium on Design and Verification of Cyber-Physical Systems: From Theory to Applications
On the occasion of Martin Fränzle's 60th birthday in October 2024, there has been a colloquium to honour his achievements and personal commitment to the scientific community during the past decades.
The colloquium took place on Friday, 28 February 2025 in the assembly hall of the Carl von Ossietzky Universität Oldenburg in Oldenburg, Germany. In the evening, the colloquium concluded with a dinner to which Martin and Barbara cordially invited.
The musical programme was performed by Andreas Peter on the grand piano.
Programme
Registration | 08:30 | ||
---|---|---|---|
Session 1 | 09:00 | Andreas Rauh | Opening |
09:15 | Werner Damm, Christoph Herrmann | Human Cyber-Physical Systems: Safety Acceptance, Social and Cultural Embeddedness | |
09:45 | Hans Langmaack, Ernst-Rüdiger Olderog | Laudatio for Martin Fränzle Laudatio by H. Langmaack (German, English) | |
10:15 | Radu Grosu | Liquid Resistance Liquid Capacitance Neural Network | |
Coffee break | 10:35 | ||
Session 2 | 11:10 | Jochem Rieger | The Challenge of Human-Cyber-Physical Systems |
11:30 | Görschwin Fey | Learning CPS Models from Observations is Impossible and Works Nicely as Illustrated by the Eysturoyartunnilin Roundabout | |
11:50 | Maike Schwammberger | Explain It for Safety: Connecting Reasoning about Conflicts with Explainability Engineering | |
12:10 | Nacim Ramdani | Set-based State Estimation for Cyber-Physical Systems: There and Back Again | |
Lunch break | 12:30 | ||
Session 3 | 13:50 | Kim Larsen, Martin Zimmermann | You May Delay, but Time Will Not: Timed Games Under Delayed Control |
14:10 | Uli Fahrenberg | Higher-Dimensional Timed Automata for Real-Time Concurrency | |
14:30 | Bai Xue | Safe Probabilistic Invariance Verification for Stochastic Discrete-time Dynamical Systems | |
Coffee break | 14:50 | ||
15:25 | Viorica Sofronie-Stokkermans | On Symbol Elimination in Theory Extensions and Applications to Parametric Verification | |
15:45 | Alessandro Abate | Keep Safe, and Reach On: Martin in the Land of Albion | |
16:05 | Jonathan Bowen | Formal Methods: Whence and Whither? | |
16:35 | Andreas Eggers | Boolean Dreams and Real Constraints: Two Decades of iSAT Solving the Undecidable | |
16:55 | Bernd Finkbeiner | Closing |
Registration
Registration was possible by personal invitation only.
Papers accepted
The following papers have been accepted for the Springer Festschrift „Design and Verification of Cyber-Physical Systems: From Theory to Applications”. The publication is in progress, news will be announced here.
- [incollection] bibtexJ. Adelt, M. Farrell, P. Herber, M. Luckcuck, and R. Monahan, Defining Contracts for Autonomous Hybrid Systems in Structured Natural Language.
- [incollection] bibtexA. Amrane, H. Bazille, E. Clement, U. Fahrenberg, and P. Schlehuber-Caissier, Higher-Dimensional Timed Automata for Real-Time Concurrency.
- [incollection] bibtexF. Bruns, A. Rauh, and M. Fnadi, Set-Based Assumption-Guarantee Reasoning for Handling Uncertainty in Functionality and Safety Verification of Dynamic Systems.
- [incollection] bibtexH. Dayekh, N. Basset, and T. Dang, Learning of Switched Nonlinear Dynamical Systems: Passive and Active Approaches.
- [incollection] bibtexJ. Ding, T. Wu, Y. Qian, L. Zhang, S. A. Deka, and B. Xue, Provable Reach-Avoid Controllers Synthesis for Deterministic Discrete-Time Systems Based on Convex Computations of Controlled Reach-Avoid Sets.
- [incollection] bibtexM. Farsang, S. A. Neubauer, and R. Grosu, Liquid Resistance Liquid Capacitance Networks.
- [incollection] bibtexB. Finkbeiner and F. Kohn, Precision in the Presence of Uncertainty: SMT-Based Runtime Validation of CPS.
- [incollection] bibtexY. Gao, C. Zhou, D. Zanarini, D. Bresolin, K. H. Johansson, and A. Abate, Sampling-Based Polytope Calculus: Computations and Applications.
- [incollection] bibtexC. Herde, T. Teige, A. Eggers, and K. Scheibler, Boolean Dreams and Real Constraints: Two Decades of iSAT Solving the Undecidable.
- [incollection] bibtexZ. Hou, H. Zhu, and J. P. Bowen, Operational and Algebraic Approaches to the Two-Run Relational System.
- [incollection] bibtexS. Khajei and J. W. Rieger, A Review of Cyber-Physical Systems in Driving: Assisting Older People.
- [incollection] bibtexJ. Kovács, E. Ábrahám, M. Niehage, and A. Remke, Martin: A Novel Mechanism for Rate Adaption in Continuous Petri Nets.
- [incollection] bibtexZ. Li, M. Yang, S. Feng, and M. Chen, Fixed-Point Reasoning for Stochastic Systems.
- [incollection] bibtexG. Lin, H. Wu, and N. Zhan, Barrier Certificate Synthesis via Interpolation and Difference-of-Convex Programming.
- [incollection] bibtexR. L. T. Mogue, N. Meslem, Y. Becis-Aubry, E. Courtial, and N. Ramdani, Secure Set-Based State Estimation of Multi-Sensor Switched Systems: An Impulsive-Switched Observer Approach.
- [incollection] bibtexC. Neurohr, L. Westhofen, T. Koopmann, E. Möhlmann, E. Böde, and A. Hahn, On Scenario Formalisms for Automated Driving.
- [incollection] bibtexE. Olderog and M. Swaminathan, Robust Structural Transformations for Real-Time Systems.
- [incollection] bibtexJ. Peleska, F. Brüning, A. E. Haxthausen, and W. Huang, A Scenario Specification Language for Testing Complex Cyber-Physical Systems.
- [incollection] bibtexM. Schmidt, S. Plambeck, and G. Fey, Learnability of Models for Cyber-Physical Systems -- A Review.
- [incollection] bibtexC. Scholl, A Review of Arithmetic Circuit Verification Using Symbolic Computer Algebra.
- [incollection] bibtexM. Schwammberger, A. Rakow, L. Putze, and A. Bairy, Explain it for Safety: Explanations for Risk Mitigation.
- [incollection] bibtexV. Sofronie-Stokkermans and P. Marohn, On Verification and Constraint Generation for Families of Similar Hybrid Automata.
- [incollection] bibtexL. Weingarten, K. Datta, S. Ahmadi-Pour, A. Kole, and R. Drechsler, Ensuring Correctness Efficiently for RISC-V Processors with Customised Multiplier Designs.
- [incollection] bibtexK. G. Larsen and M. Zimmermann, You May Delay, but Time Will Not: Timed Games Under Delayed Control.