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

[email protected]

Organisational contact

Kathrin Kuper
Carl von Ossietzky Universität Oldenburg

[email protected]

+49 441 9722 501

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 Slides
	09:45	Hans Langmaack, Ernst-Rüdiger Olderog	Laudatio for Martin Fränzle Laudatio by H. Langmaack (German, English) Slides Laudatio by E.-R. Olderog
	10:15	Radu Grosu	Liquid Resistance Liquid Capacitance Neural Network Slides
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 Slides
	11:50	Maike Schwammberger	Explain It for Safety: Connecting Reasoning about Conflicts with Explainability Engineering Slides
	12:10	Nacim Ramdani	Set-based State Estimation for Cyber-Physical Systems: There and Back Again Slides
Lunch break	12:30
Session 3	13:50	Kim Larsen, Martin Zimmermann	You May Delay, but Time Will Not: Timed Games Under Delayed Control Slides
	14:10	Uli Fahrenberg	Higher-Dimensional Timed Automata for Real-Time Concurrency Slides
	14:30	Bai Xue	Safe Probabilistic Invariance Verification for Stochastic Discrete-time Dynamical Systems Slides
Coffee break	14:50
	15:25	Viorica Sofronie-Stokkermans	On Symbol Elimination in Theory Extensions and Applications to Parametric Verification Slides
	15:45	Alessandro Abate	Keep Safe, and Reach On: Martin in the Land of Albion Slides
	16:05	Jonathan Bowen	Formal Methods: Whence and Whither? Slides
	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] bibtex
C. Herde, T. Teige, A. Eggers, and K. Scheibler, Boolean Dreams and Real Constraints: Two Decades of iSAT Solving the Undecidable. accepted 2025, to be published.
@InCollection{herde:mf60, author = {Christian Herde and Tino Teige and Andreas Eggers and Karsten Scheibler}, title = {Boolean Dreams and Real Constraints: Two Decades of iSAT Solving the Undecidable}, booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications}, year = {accepted 2025, to be published}, editor = {Andreas Rauh and Bernd Finkbeiner and Paul Kröger}, }
[incollection] bibtex
Z. Hou, H. Zhu, and J. P. Bowen, Operational and Algebraic Approaches to the Two-Run Relational System. accepted 2025, to be published.
@InCollection{hou:mf60, author = {Zhiru Hou and Huibiao Zhu and Jonathan P. Bowen}, title = {Operational and Algebraic Approaches to the Two-Run Relational System}, booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications}, year = {accepted 2025, to be published}, editor = {Andreas Rauh and Bernd Finkbeiner and Paul Kröger}, }
[incollection] bibtex
J. Kovács, E. Ábrahám, M. Niehage, and A. Remke, Martin: A Novel Mechanism for Rate Adaption in Continuous Petri Nets. accepted 2025, to be published.
@InCollection{kovacs:mf60, author = {József Kovács and Erika Ábrahám and Mathis Niehage and Anne Remke}, title = {Martin: A Novel Mechanism for Rate Adaption in Continuous Petri Nets}, booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications}, year = {accepted 2025, to be published}, editor = {Andreas Rauh and Bernd Finkbeiner and Paul Kröger}, }
[incollection] bibtex
F. Bruns, A. Rauh, and M. Fnadi, Set-Based Assumption-Guarantee Reasoning for Handling Uncertainty in Functionality and Safety Verification of Dynamic Systems. accepted 2025, to be published.
@InCollection{bruns:mf60, author = {Friederike Bruns and Andreas Rauh and Mohamed Fnadi}, title = {Set-Based Assumption-Guarantee Reasoning for Handling Uncertainty in Functionality and Safety Verification of Dynamic Systems}, booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications}, year = {accepted 2025, to be published}, editor = {Andreas Rauh and Bernd Finkbeiner and Paul Kröger}, }
[incollection] bibtex
A. Amrane, H. Bazille, E. Clement, U. Fahrenberg, and P. Schlehuber-Caissier, Higher-Dimensional Timed Automata for Real-Time Concurrency. accepted 2025, to be published.
@InCollection{amrane:mf60, author = {Amazigh Amrane and Hugo Bazille and Emily Clement and Uli Fahrenberg and Philipp Schlehuber-Caissier}, title = {Higher-Dimensional Timed Automata for Real-Time Concurrency}, booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications}, year = {accepted 2025, to be published}, editor = {Andreas Rauh and Bernd Finkbeiner and Paul Kröger}, }
[incollection] bibtex
H. Dayekh, N. Basset, and T. Dang, Learning of Switched Nonlinear Dynamical Systems: Passive and Active Approaches. accepted 2025, to be published.
@InCollection{dayekh:mf60, author = {Hadi Dayekh and Nicolas Basset and Thao Dang}, title = {Learning of Switched Nonlinear Dynamical Systems: Passive and Active Approaches}, booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications}, year = {accepted 2025, to be published}, editor = {Andreas Rauh and Bernd Finkbeiner and Paul Kröger}, }
[incollection] bibtex
Y. Gao, C. Zhou, D. Zanarini, D. Bresolin, K. H. Johansson, and A. Abate, Sampling-Based Polytope Calculus: Computations and Applications. accepted 2025, to be published.
@InCollection{gao:mf60, author = {Yulong Gao and Can Zhou and Davide Zanarini and Davide Bresolin and Karl H. Johansson and Alessandro Abate}, title = {Sampling-Based Polytope Calculus: Computations and Applications}, booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications}, year = {accepted 2025, to be published}, editor = {Andreas Rauh and Bernd Finkbeiner and Paul Kröger}, }
[incollection] bibtex
E. Olderog and M. Swaminathan, Robust Structural Transformations for Real-Time Systems. accepted 2025, to be published.
@InCollection{olderog:mf60, author = {Ernst-Rüdiger Olderog and Mani Swaminathan}, title = {Robust Structural Transformations for Real-Time Systems}, booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications}, year = {accepted 2025, to be published}, editor = {Andreas Rauh and Bernd Finkbeiner and Paul Kröger}, }
[incollection] bibtex
B. Finkbeiner and F. Kohn, Precision in the Presence of Uncertainty: SMT-Based Runtime Validation of CPS. accepted 2025, to be published.
@InCollection{finkbeiner:mf60, author = {Bernd Finkbeiner and Florian Kohn}, title = {Precision in the Presence of Uncertainty: SMT-Based Runtime Validation of CPS}, booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications}, year = {accepted 2025, to be published}, editor = {Andreas Rauh and Bernd Finkbeiner and Paul Kröger}, }
[incollection] bibtex
M. Farsang, S. A. Neubauer, and R. Grosu, Liquid Resistance Liquid Capacitance Networks. accepted 2025, to be published.
@InCollection{farsang:mf60, author = {Mónika Farsang and Sophie A. Neubauer and Radu Grosu}, title = {Liquid Resistance Liquid Capacitance Networks}, booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications}, year = {accepted 2025, to be published}, editor = {Andreas Rauh and Bernd Finkbeiner and Paul Kröger}, }
[incollection] bibtex
M. Schmidt, S. Plambeck, and G. Fey, Learnability of Models for Cyber-Physical Systems -- A Review. accepted 2025, to be published.
@InCollection{schmidt:mf60, author = {Maximilian Schmidt and Swantje Plambeck and Goerschwin Fey}, title = {Learnability of Models for Cyber-Physical Systems -- A Review}, booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications}, year = {accepted 2025, to be published}, editor = {Andreas Rauh and Bernd Finkbeiner and Paul Kröger}, }
[incollection] bibtex
Z. Li, M. Yang, S. Feng, and M. Chen, Fixed-Point Reasoning for Stochastic Systems. accepted 2025, to be published.
@InCollection{li:mf60, author = {Zhiyang Li and Mingqi Yang and Shenghua Feng and Mingshuai Chen}, title = {Fixed-Point Reasoning for Stochastic Systems}, booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications}, year = {accepted 2025, to be published}, editor = {Andreas Rauh and Bernd Finkbeiner and Paul Kröger}, }
[incollection] bibtex
G. Lin, H. Wu, and N. Zhan, Barrier Certificate Synthesis via Interpolation and Difference-of-Convex Programming. accepted 2025, to be published.
@InCollection{lin:mf60, author = {Guanhua Lin and Hao Wu and Naijun Zhan}, title = {Barrier Certificate Synthesis via Interpolation and Difference-of-Convex Programming}, booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications}, year = {accepted 2025, to be published}, editor = {Andreas Rauh and Bernd Finkbeiner and Paul Kröger}, }
[incollection] bibtex
C. Neurohr, L. Westhofen, T. Koopmann, E. Möhlmann, E. Böde, and A. Hahn, On Scenario Formalisms for Automated Driving. accepted 2025, to be published.
@InCollection{neurohr:mf60, author = {Christian Neurohr and Lukas Westhofen and Tjark Koopmann and Eike Möhlmann and Eckard Böde and Axel Hahn}, title = {On Scenario Formalisms for Automated Driving}, booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications}, year = {accepted 2025, to be published}, editor = {Andreas Rauh and Bernd Finkbeiner and Paul Kröger}, }
[incollection] bibtex
J. Peleska, F. Brüning, A. E. Haxthausen, and W. Huang, A Scenario Specification Language for Testing Complex Cyber-Physical Systems. accepted 2025, to be published.
@InCollection{peleska:mf60, author = {Jan Peleska and Felix Brüning and Anne E. Haxthausen and Wen-ling Huang}, title = {A Scenario Specification Language for Testing Complex Cyber-Physical Systems}, booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications}, year = {accepted 2025, to be published}, editor = {Andreas Rauh and Bernd Finkbeiner and Paul Kröger}, }
[incollection] bibtex
J. Adelt, M. Farrell, P. Herber, M. Luckcuck, and R. Monahan, Defining Contracts for Autonomous Hybrid Systems in Structured Natural Language. accepted 2025, to be published.
@InCollection{adelt:mf60, author = {Julius Adelt and Marie Farrell and Paula Herber and Matt Luckcuck and Rosemary Monahan}, title = {Defining Contracts for Autonomous Hybrid Systems in Structured Natural Language}, booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications}, year = {accepted 2025, to be published}, editor = {Andreas Rauh and Bernd Finkbeiner and Paul Kröger}, }
[incollection] bibtex
J. 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. accepted 2025, to be published.
@InCollection{ding:mf60, author = {Jianqiang Ding and Taoran Wu and Yuping Qian and Lijun Zhang and Shankar A. Deka and Bai Xue}, title = {Provable Reach-Avoid Controllers Synthesis for Deterministic Discrete-Time Systems Based on Convex Computations of Controlled Reach-Avoid Sets}, booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications}, year = {accepted 2025, to be published}, editor = {Andreas Rauh and Bernd Finkbeiner and Paul Kröger}, }
[incollection] bibtex
R. 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. accepted 2025, to be published.
@InCollection{mogue:mf60, author = {Ruth Line Tagne Mogue and Nacim Meslem and Yasmina Becis-Aubry and Estelle Courtial and Nacim Ramdani}, title = {Secure Set-Based State Estimation of Multi-Sensor Switched Systems: An Impulsive-Switched Observer Approach}, booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications}, year = {accepted 2025, to be published}, editor = {Andreas Rauh and Bernd Finkbeiner and Paul Kröger}, }
[incollection] bibtex
S. Khajei and J. W. Rieger, A Review of Cyber-Physical Systems in Driving: Assisting Older People. accepted 2025, to be published.
@InCollection{khajei:mf60, author = {Sina Khajei and Jochem W. Rieger}, title = {A Review of Cyber-Physical Systems in Driving: Assisting Older People}, booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications}, year = {accepted 2025, to be published}, editor = {Andreas Rauh and Bernd Finkbeiner and Paul Kröger}, }
[incollection] bibtex
C. Scholl, A Review of Arithmetic Circuit Verification Using Symbolic Computer Algebra. accepted 2025, to be published.
@InCollection{scholl:mf60, author = {Christoph Scholl}, title = {A Review of Arithmetic Circuit Verification Using Symbolic Computer Algebra}, booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications}, year = {accepted 2025, to be published}, editor = {Andreas Rauh and Bernd Finkbeiner and Paul Kröger}, }
[incollection] bibtex
M. Schwammberger, A. Rakow, L. Putze, and A. Bairy, Explain it for Safety: Explanations for Risk Mitigation. accepted 2025, to be published.
@InCollection{schwammberger:mf60, author = {Maike Schwammberger and Astrid Rakow and Lina Putze and Akhila Bairy}, title = {Explain it for Safety: Explanations for Risk Mitigation}, booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications}, year = {accepted 2025, to be published}, editor = {Andreas Rauh and Bernd Finkbeiner and Paul Kröger}, }
[incollection] bibtex
L. Weingarten, K. Datta, S. Ahmadi-Pour, A. Kole, and R. Drechsler, Ensuring Correctness Efficiently for RISC-V Processors with Customised Multiplier Designs. accepted 2025, to be published.
@InCollection{weingarten:mf60, author = {Lennart Weingarten and Kamalika Datta and Sallar Ahmadi-Pour and Abhoy Kole and Rolf Drechsler}, title = {Ensuring Correctness Efficiently for RISC-V Processors with Customised Multiplier Designs}, booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to ApplicationsDesigns}, year = {accepted 2025, to be published}, editor = {Andreas Rauh and Bernd Finkbeiner and Paul Kröger}, }
[incollection] bibtex
V. Sofronie-Stokkermans and P. Marohn, On Verification and Constraint Generation for Families of Similar Hybrid Automata. accepted 2025, to be published.
@InCollection{sofronie:mf60, author = {Viorica Sofronie-Stokkermans and Philipp Marohn}, title = {On Verification and Constraint Generation for Families of Similar Hybrid Automata}, booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications}, year = {accepted 2025, to be published}, editor = {Andreas Rauh and Bernd Finkbeiner and Paul Kröger}, }
[incollection] bibtex
K. G. Larsen and M. Zimmermann, You May Delay, but Time Will Not: Timed Games Under Delayed Control. accepted 2025, to be published.
@InCollection{zimmermann:mf60, author = {Kim G. Larsen and Martin Zimmermann}, title = {You May Delay, but Time Will Not: Timed Games Under Delayed Control}, booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications}, year = {accepted 2025, to be published}, editor = {Andreas Rauh and Bernd Finkbeiner and Paul Kröger}, }

Webmaster (Changed: 25 Mar 2025) | Kurz-URL:Shortlink: https://uole.de/p110444en

Sprache wechseln

Change Language

Hell-/Dunkelmodus

Light mode / Dark mode

Colloquium on Design and Verification of Cyber-Physical Systems: From Theory to Applications

Organisers

Organisational contact

Venue

Colloquium on Design and Verification of Cyber-Physical Systems: From Theory to Applications

Programme

Registration

Papers accepted