Student Projects

Improving Dataflow Circuit Rewrites With Trace Equivalence Checking

Inductive Proof Rules For Second-Order HyperLTL

Back to the Future: Extending RTLola with Future Offsets

Causal Analysis in Stream-Based Monitoring

Enabling APIs' for RTLola

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

Functional HDLs Meet Stream-Based Monitoring: Hardware Monitors from RTLola Using Clash

Pacing Types: Safe Monitoring of Periodic and Conditional Streams

A Neuro-symbolic Portfolio Solver for Reactive Synthesis

From Passive to Active: Scheduled Monitoring in RTLola

Contrastive Neural Model Checking

Eviction Strategies for Parameterized Streams in RTLola

Expressiveness of Hyper^2LTL

Extending RTLola with Native Support for Enumerations

Formal Verification of Symbolic Bug Finders

From Passive to Active Monitoring: A Scheduling Approach with RTLola

Leveraging Static Analysis for the RTLola User Experience

Model Checking Concurrent Hypersafety

Model Checking of HyperLTL on Finite Traces

NeuRes: A Neural Resolution Prover of Unsatisfiability

On the Relationship between Transformer Architectures and Regular Languages

Compiling RTLola Specifications

Complexity of Model Checking Second-Order Hyperproperties on Finite Structures

Counterfactual Causality in Real-Time Systems

Increasing Robustness of RTLola with Intervals

Learning Temporal Properties from Few, Positive Examples

RTLola in the Cloud: Reliability for Cloud Applications using Runtime Verification

Runtime Verification for Algorithmic Fairness

Structured Program Synthesis from Temporal Stream Logic Specifications

Synthesizing Verifiable Code for Large Specifications Using Few-Shot Learning

Talking about the Future: Predicting Stream Values for Runtime Monitoring

Verified Equivalence Checker for Omega-Regular Expressions

An Efficient Automaton Construction for Synthesizing Dominant Strategies

Complete Bounded Model Checking for Hyperproperties

Evaluation of Vulnerabilities of a Lane Keeping Assist System based on Simulations

Formal Specifications from Natural Language

Generating and Solving Temporal Logic Problems with Adversarial Transformers

Model Checking Temporal Stream Logic and Hyper-Temporal Stream Logic

Model-Refinement via Runtime Monitoring

Modularization of code in RTLola

Predicting Timed Traces with Neural Networks

Refinement of TSL Specifications for LTL Synthesis

Repairing Circuits with Transformers

RTLola App

Runtime Monitoring of Neural Networks for Safe Autonomous Driving

Visuallizing Game-Based Certificates for Hyperproperty Verification

Algorithms for Deciding HyperCTL*

Bounded Model Checking for PHL

Causal Solving of Reachability Games

LTL Synthesis from Specification Patterns with Neural Networks

MCHyper Reimplementation: Conception

MCHyper Reimplementation: Conception and Execution

Monitoring HyperMTL

Monitoring Smart Contracts with RTLola

Outlier Prediction in Image Streams

Robust Runtime Verification for Medical CPS

Timing is Key - A WCET Analysis of RTLola

Satisfiability of Temporal Stream Logic modulo Theories

Specification Decomposition for Reactive Synthesis

Synthesizing Epistemic Specifications Using LTL Synthesis

Temporal Stream Logic for Hyperproperties

Tracing Correctness: A Practical Approach to Traceable Runtime Monitoring

Trajectory Prediction with RNNs

Verifiable Runtime Monitor Generation for Lola Specifications

A Stream-based Approach to Network Intrusion Detection

Causality-Based Model Checking for Real-Time Systems

Compiling Lola 2.0 to C

Compositional Synthesis of Dominant Strategies for Distributed Systems

Generating Concurrency-preserving Petri Games

Learning the Desired Behavior for Causality Analyses

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

Live Synthesis

Monitoring Hybrid Automata

Syntroids

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

Translating Asynchronous Games for Distributed Synthesis

Verifying Hyperliveness

Bounded Synthesis for Past LTL

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

Learning Hyperproperties

MCHyper Online Interface: Backend

MCHyper Online Interface: Frontend

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

Model Checking Timed Hyperproperties

Runtime Verification of Critical Web-based Systems with Lola

Bounded Synthesis of Petri Games with True Concurrency Semantics

Bounded Synthesis of Reactive Programs

Comparing Lola 2.0 with Quantitative Regular Expressions

Encodings of Bounded Synthesis of Distributed Systems

FPGA-based Monitoring for Stream Specification Languages

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

Learning Automata for LTL

Synthesis and Analysis of Strategies for Automatic Parking Garages

Synthesis for Petri Games with One System Player

A Proof System for HyperLTL

Bounded Synthesis for HyperLTL

Equivalence of Petri Games

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

Runtime Verification with LOLA

A Game-Based Semantis for CSP

A Specification Format for Reactive Synthesis

Approximate LTL Model Counting

Bounded Synthesis for Distributed Architectures

Heuristic Algorithms for the Synthesis of AIGER Circuits

Monitoring First-order Parametric Temporal Logic

Optimizing LOLA Specifications

Strategies in Regular Delay Games

Solving Büchi Games

Concept Learning for Reactive Synthesis

Detecting Unrealizable Specifications of Distributed Systems

Slicing Abstractions for Modular Programs

Slicing Abstractions for Safety Games

Spin the Records: Synthesizing Electronic Dance Music Using Model Checking Methods

Synthesis of Distributed Reactive Programs

Synthesis of Dominant Strategies

A compositional proof rule for Extended Coordination Logic

Acceleration of Timed Automata

Automatische Verifikation von Petri-Netzen mit SLAB

Decidability of Semilinear Petri Games

Game-based analysis of timed business processes

Model Measuring

Small strategies for safety games

Fully Symbolic Model Checking using Constraint Matrix Diagrams

Zone State Diagrams – Model Checking Data-Intensive Real-Time Systems

Clock Matrix Diagrams

From Uppaal to Slab

Optimal Schedulers for Time-Bounded Reachability in CTMDPs

Symbolic Encodings of Timed Games with Incomplete Information

Verifying Networks of Phase Event Automata

Minimization of Tree Automata

Deductive Model Checking with Transition Constraint Systems

Symbolic Game Solving with Arithmetic Data Types

Translation Validation for Optimizing Compilers

Automatic Abstraction of Synchronization Sequences

Learning Minimal Requirements for Compositional Verification

Automatic Verification of Conditions for Absence of Interrupts

Controller Program Synthesis for Industrial Machines

Distributed Games For Reactive Systems

Monitoring Execution Traces using Metric Alternating Automata

Synthesis of Reactive Systems