Event Category: MSc Defence

–

On Thursday 1 October 2026, 14:00-15:00, MF 3.122, Huaze will defend his Master thesis project titled Shielding for Autonomous Highway Driving with STARK Abstract: Reinforcement-learning-based autonomous driving agents can achieve effective driving behaviours, but their decisions are difficult to verify and may lead to unsafe situations. This thesis studies runtime safety shielding for the ABZ …continue reading

–

Wietske will defend her Master Project thesis titled “Modelling a Mechanical Lung Ventilator in Stark”. Abstract: In this Master Thesis a Stark model of a Mechanical Lung Ventilator (MLV) is presented. In particular, the specification document of the MLV from the ABZ 2024 case study is used. Requirements from the case study have been transformed …continue reading

–

Binary Decision Diagrams (BDDs) are widely used to efficiently encode and visually represent Boolean functions. BDDs use recursive algorithms to apply logical operators, which makes the manipulation and reduction of Boolean functions more efficient. BDDs can also be used to analyze the behavior of a Boolean function due to the branching structure of the BDD, …continue reading

–

In [1] various template formulas are presented that describe states that adhere to different liveness properties and completeness criteria. To draw reliable conclusions from verifications using these formulas, their correctness is critical. The formulas are informally proven correct, but handwritten proofs demand attention to detail of the writer and are sometimes found to be imprecise. …continue reading

–

Context-Free-Language Ordered Binary Decision Diagrams form an alternative to Binary Decision Diagrams. CFLOBDDs aim to minimize the space required to encode Boolean functions by reusing repeated patterns. This way CFLOBDDs can be exponentially smaller than their BDD counterparts. In this thesis, we investigate the effectiveness of CFLOBDDs for model checking. To this end, we evaluate the space …continue reading

–

TSP;ac, the theory of sequential processes with sequencing, attributes, and conditions, was previously created as a simplification of TSP;ps, which exists for the sake of a process theoretic counterpart to the classical correspondence between pushdown automata and context-free grammars. This theory has a mechanism called sequential value passing, used to transfer data between sequential processes. …continue reading

–

Abstract: State systems are often represented by some type of graph, such as Kripke Structures (KSs) or Labeled Transition Systems (LTSs). There is a broad spectrum of equivalences that specify if two states are behaviorally “the same”, some of which can be efficiently computed, such as strong bisimilarity and branching bisimilarity. There do not exist …continue reading

–

This thesis investigates the axiomatisability of weak decorated trace semantics over the process algebra BCCS extended with the interleaving parallel composition operator, denoted as BCCS∥. Weak semantics consider the silent action τ as an invisible action to abstract away from internal behaviour. The weak decorated trace semantics consist of weak trace, weak completed trace, weak …continue reading

–

On 31 March at 14:00, Mara Miulescu will defend her MSc thesis titled “Computer-Assisted Verification of Partial-Order Reduction Methods”. A summary of her work is given below. Proving a complex theory correct is difficult; finding a counterexample decades after its publication is even tougher. Recently, correctness issues have been uncovered in several partial-order reduction (POR) …continue reading