Publications

A Deductive System for Contract Satisfaction Proofs

Flowing Through States: ODE Regularization for Reinforcement Learning

Pacing Types for Asynchronous Stream Equations

Universal Safety Controllers with Learned Prophecies

Back to the Future: Extending RTLola with Future Offsets

Strategy Logic, Imperfect Information, and Hyperproperties

An Information-Flow Perspective on Explainability Requirements: Specification and Verification

On Conformant Planning and Model-Checking of ∃*∀* Hyperproperties

Almost Fair Simulations

Explainability Requirements as Hyperproperties

Verifying Asynchronous Hyperproperties in Reactive Systems

On Hyperproperty Verification, Quantifier Alternations, and Games under Partial Information

Pacing Types: Safe Monitoring of Periodic and Conditional Streams

A ROS Adapter for RTLola

Active Monitoring with RTLola: A Specification-Guided Scheduling Approach

Tiny Drone, Tiny Resources: Deploying RTLola Monitors on the Crazyflie Platform

An Intermediate Program Representation for Optimizing Stream-Based Languages

Robust Runtime Monitoring with Slack Variables

Predicate abstraction for hyperliveness verification

Closure and Complexity of Temporal Causality

Multiplayer Games With Incomplete Information for Hyperproperty Verification (Extended Abstract)

AutoHyper: leveraging language inclusion checking for hyperproperty model-checking

Stream-Based Monitoring of Algorithmic Fairness

Synthesis of Universal Safety Controllers

Coinductive Proofs for Temporal Hyperliveness

From RTLola to SRTLola: A Block-Based Syntax for Stream-Based Specification Languages

Learning Better Representations from Less Data for Propositional Satisfiability

Counterfactual Explanations for MITL Violations

Checking Satisfiability of Hyperproperties using First-Order Logic

Stream-Based Monitoring Under Measurement Noise

Finding ∀∃ Hyperbugs using Symbolic Execution

A Tutorial on Stream-Based Monitoring

Visualizing Game-Based Certificates for Hyperproperty Verification

Information Flow Guided Synthesis with Unbounded Communication

Syntax-Guided Automated Program Repair for Hyperproperties

Monitoring Unmanned Aircraft: Specification, Integration, and Lessons-Learned

Synthesis of Temporal Causality

Non-Deterministic Planning for Hyperproperty Verification

Temporal Behavior Trees -- Segmentation

Temporal Behavior Trees: Robustness and Segmentation

Hyper Strategy Logic

Monitoring Second-Order Hyperproperties

Automated Software Verification of Hyperliveness

NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesis

On Alternating-Time Temporal Logic, Hyperproperties, and Strategy Sharing

NeuRes: A Neural Resolution Prover of Unsatisfiability

À la recherche de tous les vrais bugs (Searching All True Bugs)

Formal Verification of Symbolic Bug Finders

Certification Aspects of Runtime Assurance for Urban Air Mobility

From Passive to Active Monitoring: A Scheduling Approach with RTLola

Engineering a Formally Verified Automated Bug Finder

Learning Temporal Properties from Few, Positive Examples

Checking and Sketching Causes on Temporal Sequences

Leveraging Static Analysis: An IDE for RTLola

Reactive Synthesis of Smart Contract Control Flows

Synthesizing Verifiable Code for Large Specifications Using Few-Shot Learning

Concurrent Hyperproperties

Verified Equivalence Checker for Omega-Regular Expressions

Neural Circuit Synthesis with Pre-trained Language Models

nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models

Second-Order Hyperproperties

Smart Contract Synthesis Modulo Hyperproperties

Counterfactual Causality in Real-Time Systems

Counterfactuals Modulo Temporal Logics

Model Checking Omega-Regular Hyperproperties with AutoHyperQ

HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems

Automata-Based Software Model Checking of Hyperproperties

Iterative Circuit Repair Against Formal Specifications

Logics and Algorithms for Hyperproperties

AutoHyper: Explicit-State Model Checking for HyperLTL

Inferring Symbolic Automata

Runtime Verification for Algorithmic Fairness

A Hierarchy of Monitoring Properties for Autonomous Systems

Complexity of Model Checking Second-Order Hyperproperties on Finite Structures

Automated Program Repair Using Formal Verification Techniques

Synthesizing Dominant Strategies for Liveness

Temporal Causality in Reactive Systems

Assume, Guarantee or Repair – a Regular Framework for non-Regular Properties

Real-time Visualization of Stream-based Monitoring Data.

Realizable and Context-Free Hyperlanguages

Repairing Circuits with Transformers

Explaining Hyperproperty Violations

Information Flow Guided Synthesis

Deciding Hyperproperties Combined with Functional Specifications

Monitoring with Verified Guarantees

Prophecy Variables for Hyperproperty Verification

Software Verification of Hyperproperties Beyond k-Safety

Specification decomposition for reactive synthesis

Guaranteed Bounds for Posterior Inference in Universal Probabilistic Programming

Can reactive synthesis and syntax-guided synthesis be friends?

Complete Bounded Model Checking for Hyperproperties

BOCoSy: Small but Powerful Symbolic Output-Feedback Control

Predicting Timed Traces With Neural Networks

A Truly Robust Signal Temporal Logic: Monitoring Safety Properties of Interacting Cyber-Physical Systems under Uncertain Observation

Compositional synthesis of modular systems

Live synthesis

Temporal Stream Logic modulo Theories

Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory

Inferring Symbolic Automata

Generating and Solving Temporal Logic Problems with Adversarial Transformers

FLoBC: A Decentralized Blockchain-Based Federated Learning Framework

Model Checking Temporal Stream Logic and Hyper-Temporal Stream Logic

Modularization of code in RTLola

Refinement of TSL Specifications for LTL Synthesis

Synthesis of Asynchronous Distributed Systems from Global Specifications

Linear-time Temporal Logic with Team Semantics: Expressivity and Complexity

Neural Circuit Synthesis from Specification Patterns

Visual Analysis of Hyperproperties for Understanding Model Checking Results

Compositional Synthesis of Modular Systems

Live Synthesis

Runtime Enforcement of Hyperproperties

Monitoring with Verified Guarantees

Deep Learning for Temporal Logics

A Temporal Logic for Strategic Hyperproperties

A Temporal Logic for Asynchronous Hyperproperties

Causality-Based Game Solving

On Probabilistic Termination of Functional Programs with Continuous Distributions

Specification Decomposition for Reactive Synthesis

Automatic Optimizations for Runtime Verification Specifications

Robust Monitoring for Medical Cyber-Physical Systems

Teaching Temporal Logics to Neural Networks

A Web Interface for Petri Nets with Transits and Petri Games

RTLola on Board: Testing Real Driving Emissions on your Phone

Causal Solving of Reachability Games

Modeling and Verifying the FlexRay Physical Layer Protocol with Reachability Checking of Timed Automata

Robust Monitoring of Medical Cyber-Physical Systems

Model Checking Algorithms for Hyperproperties (Invited Paper)

Bounded Model Checking for PHL

Monitoring Smart Contracts with RTLola

Timing is Key - A WCET Analysis of RTLola

Dependency-based Compositional Synthesis

Explainable Reactive Synthesis

Model Checking Branching Properties on Petri Nets with Transits

Probabilistic Hyperproperties of Markov Decision Processes

Automatic Optimizations for Stream-based Monitoring Languages

Monitoring Cyber-Physical Systems: From Design to Integration

On Termination of Higher-Order Recursive Programs with Continuous Distributions

Verified Rust Monitors for Lola Specifications

Synthesizing Stream Control

The Hierarchy of Hyperlogics: A Knowledge Reasoning Perspective

Controller Synthesis for Hyperproperties

Transformers Generalize to the Semantics of Logics

AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL

Realizing Omega-regular Hyperproperties

RTLola Cleared for Take-Off: Monitoring Autonomous Aircraft

Assume, Guarantee or Repair

From LTL to rLTL Monitoring: Improved Monitorability through Robust Semantics

Simplex Architecture Meets RTLola

Specification-Aided Trajectory Prediction with RNNs

Efficient monitoring of hyperproperties using prefix trees

Verifiable Runtime Monitor Generation for Lola Specifications

Tracing Correctness: A Practical Approach to Traceable Runtime Monitoring

How to Win First-Order Safety Games

Temporal Stream Logic for Hyperproperties

Model Counting for Reactive Systems

Symbolic Reactive Synthesis

Synthesis from Hyperproperties

Stream-based Monitors for Real-time Properties

Approximate Automata for Omega-regular Languages

Efficient Trace Encodings of Bounded Synthesis for Asynchronous Distributed Systems

Model Checking Data Flows in Concurrent Network Updates

Program Repair for Hyperproperties

Syntroids: Synthesizing a Game for FPGAs using Temporal Logic Specifications

FPGA Stream-Monitoring of Real-time Properties

On the Similarities of Aircraft and Humans: Monitoring CPS with StreamLAB

Algorithms for Monitoring Hyperproperties

A Stream-based Approach to Network Intrusion Detection

Verifying Hyperliveness

Let’s not Trust Experience Blindly: Formal Monitoring of Humans and other CPS

Monitoring Hybrid Automata

Towards Synthesizing Smart Contracts: Reducing ATL* Synthesis to HyperLTL Synthesis

Translating Asynchronous Games for Distributed Synthesis

Synthesizing Functional Reactive Programs

Translating Asynchronous Games for Distributed Synthesis

StreamLAB: Stream-based Monitoring of Cyber-physical Systems

Synthesizing Approximate Implementations for Unrealizable Specifications

Temporal Stream Logic: Synthesis beyond the Bools

Verifying Hyperliveness

Learning Desired Behavior for Causality Analysis

Clausal Abstraction for DQBF

Causality and Hyperproperties

Canonical Representations of k-Safety Hyperproperties

Monitoring Hyperproperties

The Hierarchy of Hyperlogics

Monitoring with Parameters

Clausal Abstraction for DQBF (full version)

Real-time Stream Monitoring with StreamLAB

Optimality and Resilience in Parity Games

Constraint-based Monitoring of Hyperproperties

Causality-Based Model Checking for Real-Time Systems

Compiling Lola 2.0 to C

Generating Concurrency-preserving Petri Games

Visibly Linear Dynamic Logic

An Automata-Theoretic Approach to Model-Checking Systems and Specifications Over Infinite Data Domains

A Symbolic Algorithm for Lazy Synthesis of Eager Strategies

Bounded Synthesis of Reactive Programs

Runtime Verification of Critical Web-based Systems with Lola

Distributed Synthesis for Parameterized Temporal Logics

Bounded Synthesis for Past LTL

Quantitative Reductions and Infinite Vertex-Ranked Games

Solving QBF by Abstraction

Synthesizing Optimally Resilient Controllers

Team Semantics for the Specification and Verification of Hyperproperties

Robust, Expressive, and Quantitative Linear Temporal Logics: Pick any Two for Free

Model Checking Quantitative Hyperproperties

Synthesizing Reactive Systems from Hyperproperties

Understanding and Extending Incremental Determinization for 2QBF

The Complexity of Monitoring Hyperproperties

Model Checking Timed Hyperproperties

Parity to Safety in Polynomial Time for Pushdown and Collapsible Pushdown Systems

The Challenges in Specifying and Explaining Synthesized Implementations of Reactive Systems

Parity Games with Weights

Parameterized Linear Temporal Logics Meet Costs: Still not Costlier than LTL

The Complexity of Counting Models of Linear-time Temporal Logic

RVHyper: A Runtime Verification Tool for Temporal Hyperproperties

MGHyper: Checking Satisfiability of HyperLTL Formulas beyond the ∃*∀*-Fragment

HyperLTL Synthesis

Analyzing Guarded Protocols: Better Cutoffs, More Systems, More Expressivity

Proceedings of the Sixth Workshop on Synthesis (SYNT 2017)

The 4th Reactive Synthesis Competition <notextile>(SYNTCOMP 2017)</notextile>: Benchmarks, Participants and Results

Bounded Synthesis of Reactive Programs

From Knowledge- to Belief-Based Programming for Mobile Ad-Hoc Networks

Verifying Security Policies in Multi-agent Workflows with Loops

Encodings of Bounded Synthesis of Distributed Systems

Bounded Synthesis of Petri Games with True Concurrency Firing Semantics

Reactive Synthesis: Towards Output-Sensitive Algorithms

Symmetric Synthesis

Synthesis in Distributed Environments

Causality-based Model Checking

The Density of Linear-time Properties

Temporal Hyperproperties

Finite-state Strategies in Delay Games

Easy to Win, Hard to Master: Optimal Strategies in Parity Games with Costs

Synthesizing Optimally Resilient Controllers

Monitoring Hyperproperties

Stream Runtime Monitoring on UAS

Satisfiability and Monitoring of Hyperproperties

VLDL Satisfiability and Model Checking via Tree Automata

BoSy: An Experimentation Framework for Bounded Synthesis

EAHyper: Satisfiability, Implication, and Equivalence Checking of Hyperproperties

On Expansion and Resolution in CEGAR Based QBF Solving

Symbolic vs. Bounded Synthesis for Petri Games

Team Semantics for the Specification and Verification of Hyperproperties

Distributed Synthesis for Parameterized Temporal Logics

Finite-state Strategies in Delay Games (full version)

Is your software on dope? ⋆ Formal analysis of surreptitiously “enhanced” programs

Quantitative Reductions and Infinite Vertex-Ranked Games

Bounding Average-energy Games

Encodings of Bounded Synthesis

Vehicle Platooning Simulations with Functional Reactive Programming

An Automata-Theoretic Approach to Modeling Systems and Specifications over Infinite Data

Parametric Linear Dynamic Logic

The First-Order Logic of Hyperproperties

Towards Intelligent System Health Management using Runtime Monitoring

Games with Costs and Delays

Visibly Linear Dynamic Logic

Causality-based Verification

Provable State-Space Minimization of Büchi Automata arising from LTL Specifications

A High-Level LTL Synthesis Format: TLSF v1.1

The Reactive Synthesis Competition: SYNTCOMP 2016 and Beyond

The Third Reactive Synthesis Competition <notextile>(SYNTCOMP 2016)</notextile>: Benchmarks, Participants and Results

Delay Games with WMSO+U Winning Conditions

Runtime Monitoring with Lola

Limit Your Consumption! Finding Bounds in Average-energy Games

Bounding Average-energy Games

The First-Order Logic of Hyperproperties

Synthesizing Skeletons for Reactive Systems

Specifying and Verifying Secrecy in Workflows with Arbitrarily Many Agents

Facets of Software Doping

Petri Games: Synthesis of Distributed Systems with Causal Memory

A Stream-based Specification Language for Network Monitoring

Approximating Optimal Bounds in Prompt-LTL Realizability in Doubly-exponential Time

Distributed PROMPT-LTL Synthesis

Deciding Hyperproperties

How Much Lookahead is Needed to Win Infinite Games?

Synthesis of Self-Stabilizing and Byzantine-Resilient Distributed Systems

What You Really Need To Know About Your Neighbor

Bounded Cycle Synthesis

Equivalence of Petri Games

Non-prenex QBF Solving Using Abstraction

Decidability in Parameterized Verification

Synthesis of Reactive Systems

Easy to Win, Hard to Master: Optimal Strategies in Parity Games with Costs

A Temporal Logic Approach to Information-flow Control

The First Reactive Synthesis Competition <notextile>(SYNTCOMP 2014)</notextile>

Prompt Delay

A Proof System for HyperLTL

Deciding HyperLTL

The Second Reactive Synthesis Competition <notextile>(SYNTCOMP 2015)</notextile>

Tight Cutoffs for Guarded Protocols with Fairness

Visibly Linear Dynamic Logic

Optimal Strategy Synthesis for Request-Response Games

Approximating Optimal Bounds in Prompt-LTL Realizability in Doubly-exponential Time

CAQE: A Certifying QBF Solver

Automata Tutor and what we learned from building an online teaching tool

Limit Your Consumption! Finding Bounds in Average-energy Games

Optimizing LOLA Specifications

Decidability of Parameterized Verification

Unbounded Lookahead in WMSO+U Games

Distributed PROMPT-LTL Synthesis

Bounded Synthesis of Distributed Architectures

Bounded Synthesis for Petri Games

Analyzing Arithmetic Prolog Programs by Symbolic Execution

Detecting Unrealizability of Distributed Fault-tolerant Systems

ADAM: Causality-Based Synthesis of Distributed Systems

Algorithms for Model Checking HyperLTL and HyperCTL*

Delay Games with WMSO+U Winning Conditions

How much lookahead is needed to win infinite games?

Problem Generation for DFA Construction

Parameterized Linear Temporal Logics Meet Costs: Still not Costlier than LTL

Poster<notextile>:</notextile> Security in Web-Based Workflows

A Game-Based Semantics for CSP

Monitoring First-order Parametric Linear-time Temporal Logic

Approximate LTL Model Counting

Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information

What are Strategies in Delay Games? Borel Determinacy for Games with Lookahead

Delay Games with WMSO+U Winning Conditions

How much lookahead is needed to win infinite games?

Synthesis and Control of Infinite-State Systems with Partial Observability

The Complexity of Counting Models of Linear-time Temporal Logic

Down the Borel Hierarchy: Solving Muller Games via Safety Games

The Linear-Hyper-Branching Spectrum of Temporal Logics

Parametric Linear Dynamic Logic

Petri Games: Synthesis of Distributed Systems with Causal Memory

Symbolic Approximation of the Bounded Reachability Probability in Large Markov Chains

Fast DQBF Refutation <notextile>(full version)</notextile>

Fast DQBF Refutation

Causal Termination of Multi-threaded Programs

Parity and Streett Games with Costs

Optimal Strategy Synthesis for Request-Response Games

Automatic Compositional Synthesis of Distributed Systems

A shallow embedding of HyperCTL*

Detecting Unrealizable Specifications of Distributed Systems

Temporal Logics for Hyperproperties

Counting Models of Linear-time Temporal Logic

Monitoring Parametric Temporal Logic

Relational Abstract Interpretation for the Verification of 2-Hypersafety Properties

Symmetric and Efficient Synthesis

Bounded Synthesis

A Uniform Approach to the Complexity and Analysis of Succinct Systems

Causality-Based Verification of Multi-threaded Programs

Optimal Bounds in Parametric LTL Games

A Temporal Logic for Hyperproperties

Lossy Channel Games under Incomplete Information

Optimal time-abstract schedulers for CTMDPs and continuous-time Markov games

Cost-Parity and Cost-Streett Games

Symbolically Synthesizing Small Circuits

Efficient Parallel Path Checking for Linear-Time Temporal Logic With Past and Bounds

Monitoring Temporal Information Flow

ALLQBF Solving by Computational Learning

Verification of Partial-Information Probabilistic Systems Using Counterexample-Guided Refinements

Parity and Streett Games with Costs

Counterexample-guided Synthesis of Observation Predicates

The Complexity of Bounded Synthesis for Timed Control with Partial Observability

Down the Borel Hierarchy: Solving Muller Games via Safety Games

Playing Pushdown Parity Games in a Hurry

ACTL ∩ LTL Synthesis

Sparse Positional Strategies for Safety Games

FlexRay for Avionics: Automatic Verification with Parametric Physical Layers

Automatic Protocol Verification with Parametric Physical Layers

Playing Muller Games in a Hurry

Symbolic Bounded Synthesis

Template-based Controller Synthesis for Timed Systems

Lazy Synthesis

Model Checking Information Flow in Reactive Systems

Solving Infinite Games with Bounds

Efficient Approximation of Optimal Control for Continuous-Time Markov Games

Monitoring Realizability

Weak Kripke Structures and LTL

Degrees of Lookahead in Context-free Infinite Games

Small witnesses, accepting lassos and winning strategies in omega-automata and games

Finite Optimal Control for Time-bounded Reachability in CTMDPs and Continuous-time Markov Games

Synthia: Verification and Synthesis for Timed Automata

Optimal Bounds in Parametric LTL Games

Solving Muller Games via Safety Games

Does It Pay to Extend the Perimeter of a World Model?

Reactive Safety

Generalized Rabin(1) Synthesis with Applications to Robust System Synthesis

Unbeast: Symbolic Bounded Synthesis

Experimental Aspects of Synthesis

Subsequence Invariants

Model Checking Finite Paths and Trees

Degrees of Lookahead in Context-free Infinite Games

Fully Symbolic Timed Model Checking using Constraint Matrix Diagrams

Zone State Diagrams

Making the Right Cut in Model Checking Data-Intensive Timed Systems

Efficient Approximation of Optimal Control for Markov Games - early arXiv version

On the Virtue of Patience: Minimizing Büchi Automata

Model Checking the FlexRay Physical Layer Protocol

Combining Symbolic Representations for Solving Timed Games

Coordination Logic

Minimising Deterministic Büchi Automata Precisely using SAT Solving

Symbolic Bounded Synthesis

Synthesising Certificates in Networks of Timed Automata

Optimal Time-Abstract Schedulers for CTMDPs and Markov Games

Parametric LTL Games

Short Witnesses and Accepting Lassos in omega-automata

Finite Optimal Control for Time-Bounded Reachability in CTMDPs and Continuous-Time Markov Games

SLAB: A Certifying Model Checker for Infinite-State Concurrent Systems

Generalised Rabin(1) synthesis

Playing Muller Games in a Hurry

Component-based Abstraction Refinement for Timed Controller Synthesis

Synthesis of Fault-Tolerant Distributed Systems

From Uppaal to Slab

LTL Path Checking is Efficiently Parallelizable

Time-optimal Winning Strategies for Poset Games

Monitor Circuits for LTL with Bounded and Unbounded Future

Clock Matrix Diagrams

Verifying Networks of Phase Event Automata

Symbolic Encodings of Timed Games with Incomplete Information

Time-optimal Winning Strategies in Infinite Games

Slicing Abstractions

Abstraction Refinement for Games with Incomplete Information

Synthesizing Certificates in Networks of Timed Automata

Directed Model Checking with Distance-preserving Abstractions

Subsequence Invariants

RESY: Requirement Synthesis for Compositional Model Checking

Synthesis of Distributed Systems

An Optimal Strategy Improvement Algorithm for Solving Parity and Payoff Games

Is Lazy Abstraction a Decision Procedure for Broadcast Protocols?

ATL* Satisfiability is 2EXPTIME-complete

Translation Validation for Optimizing Compilers

Proceedings of the Fourth Workshop on Model Based Testing (MBT 2008)

Proceedings of the Third Workshop on Model Based Testing (MBT 2007)

UPPAAL/DMC – Abstraction-based Heuristics for Directed Model Checking