Projects & publications

Research on formal verification and correct-by-design control of stochastic and learning-enabled systems — with a focus on quantified, data-driven safety guarantees.

Google Scholar → Full list below

01 — Projects

Research Tracks

Neurosymbolic representations

Vision-Based Autonomy

Learning latent neurosymbolic representations that act as sufficient statistics — enabling us to monitor and control vision-based systems efficiently and with formal guarantees.

To be presented at CDC 2026

Vision-Based Runtime Monitoring under Varying Specifications using Semantic Latent Representations

A reusable, certified runtime monitor that infers safety-relevant quantities directly from images and certifies an entire fragment of temporal-logic specifications with a single conformal calibration pass — validated on real-world Waymo driving data.

Pre-print

Multi-objective reasoning

Robust Multi-Objective Reasoning

Balancing competing objectives under uncertainty — from multi-objective physics-guided models of dynamical systems to spatiotemporal robustness of temporal-logic tasks.

CAV 2026

Spatiotemporal Robustness of Temporal-Logic Tasks using Multi-Objective Reasoning

Jointly reasons about the spatial and temporal robustness of signal temporal logic tasks, trading them off through a multi-objective formulation.

Full paper

IFAC ALCOS 2022

Multi-Objective Physics-Guided Recurrent Neural Networks for Identifying Non-Autonomous Dynamical Systems

Embeds physical priors into recurrent networks via a multi-objective training scheme, sharpening identification of non-autonomous dynamics.

Full paper

Learning-enabled certification

LUCID

Certifies black-box stochastic systems from a finite dataset of transitions — the first tool to give quantified safety guarantees.

Try LUCID

AAAI 2025

LUCID: Learning-enabled Uncertainty-aware Certification of Stochastic Dynamical Systems

Introduces the verification engine and its quantified guarantees for black-box stochastic systems.

Full paper Tool

JAIR 2026

Kernel-Based Learning of Safety Barriers

Establishes the theory behind LUCID via kernel methods and conditional mean embeddings.

Full paper

ACC 2024

Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates & Conditional Mean Embeddings

Solves the program for unknown polynomial dynamics efficiently using sum-of-squares optimization.

Full paper

Controller synthesis

SySCoRe

Correct-by-design control for uncertain stochastic systems via stochastic simulation relations, scaled with tensor representations.

Try online

HSCC 2023

SySCoRe: Synthesis via Stochastic Coupling Relations

The MATLAB toolbox for synthesizing robust controllers with formal robustness guarantees.

Full paper

IEEE TAC 2024

Bayesian Formal Synthesis of Unknown Systems via Robust Simulation Relations

Data-driven correct-by-design synthesis combining simulation relations with Bayesian linear regression.

Full paper

IEEE CDC 2023

Verifying the Unknown: Correct-by-Design Control Synthesis for Networks of Stochastic Uncertain Systems

Extends sub-simulation relations to compositional systems with arbitrary additive noise.

Full paper

QEST 2025

Formal Control for Uncertain Systems via Contract-Based Probabilistic Surrogates

An adversarial framework that scales probabilistic simulation relations by removing explicit error bounds.

Full paper

Scalable abstraction

Binary-Tree Gaussian Processes

Data-driven abstractions that naturally partition the state space, simplifying error quantification for formal verification.

IFAC ADHS 2024

Data-Driven Abstractions via Binary-Tree Gaussian Processes for Formal Verification

BTGPs partition the state space to yield formal models amenable to model checking.

Full paper

Complete list

All publications

Citation counts via Google Scholar.

Title	Authors	Cites	Year
Spatiotemporal robustness of temporal logic tasks using multi-objective reasoning · CAV	O Schön, L Lindemann	1	2026
Multi-Objective Reasoning · CAV 2026, Lisbon	O Schön, L Lindemann	—	2026
Kernel-Based Learning of Safety Barriers · JAIR	O Schön, Z Zhong, S Soudjani	2	2026
Vision-Based Runtime Monitoring under Varying Specifications using Semantic Latent Representations	B Hoxha, O Schön, H Okamoto, L Lindemann, G Fainekos	—	2026
Safety Certification is Classification · arXiv	O Schön, L Romao, S Soudjani	—	2026
LUCID: Learning-enabled uncertainty-aware certification of stochastic dynamical systems · AAAI	E Casablanca, O Schön, P Zuliani, S Soudjani	4	2026
Formal Control for Uncertain Systems via Contract-Based Probabilistic Surrogates · QEST	O Schön, S Haesaert, S Soudjani	1	2025
Bayesian formal synthesis of unknown systems via robust simulation relations · IEEE TAC	O Schön, B van Huijgevoort, S Haesaert, S Soudjani	18	2024
Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates & Conditional Mean Embeddings · ACC	O Schön, Z Zhong, S Soudjani	14	2024
Lyapunov-based policy synthesis for multi-objective interval MDPs · IFAC	N Monir, O Schön, S Soudjani	3	2024
Data-driven abstractions via binary-tree Gaussian processes for formal verification · IFAC	O Schön, S Naseer, B Wooding, S Soudjani	9	2024
Verifying the unknown: correct-by-design control synthesis for networks of stochastic uncertain systems · IEEE CDC	O Schön, B van Huijgevoort, S Haesaert, S Soudjani	9	2023
Data-Driven Correct-by-Design Control of Parametric Stochastic Systems · HSCC (poster)	O Schön, B van Huijgevoort, S Haesaert, S Soudjani	—	2023
SySCoRe: Synthesis via stochastic coupling relations · HSCC	B van Huijgevoort, O Schön, S Soudjani, S Haesaert	29	2023
ARCH-COMP23 category report: stochastic models · EPiC	A Abate, H Blom, N Cauchi, S Haesaert, B van Huijgevoort, O Schön, et al.	9	2023
Correct-by-Design Control of Parametric Stochastic Systems · IEEE CDC	O Schön, B van Huijgevoort, S Haesaert, S Soudjani	11	2022
Multi-Objective Physics-Guided Recurrent Neural Networks for Identifying Non-Autonomous Dynamical Systems · IFAC ALCOS	O Schön, R Samantha-Götte, J Timmermann	—	2022
ARCH-COMP22 category report: stochastic models · ARCH22	A Abate, O Schön, et al.	—	2022

View full profile on Google Scholar →

Theses

Dissertations

Master's Thesis — Physics-Guided Neural Networks for the Identification of Dynamical Systems

First investigation of PGNNs for dynamic-system identification from a control-engineering viewpoint. A Physics-guided Recurrent Neural Network substantially outperforms purely data-driven approaches; physics-based constraints further compensate for inaccurate dynamics models. (in German)

Full text →

Pre-Master's Thesis — Efficient Bayesian Optimization using A-Priori Knowledge

Examines how physically-grounded prior knowledge accelerates Bayesian optimization. Sufficiently accurate priors significantly increase optimizer efficiency; problem conditioning and dimensionality play key roles. (in German)

Full text →

Network