The MOVES seminar is bi-weekly on Tuesdays at 10:00. It takes place in the virtual room at https://rwth.zoom.us/my/moves. (When a different URL is used for a specific talk, this will be indicated with a *.)

If you want to give a talk, please inform Alexander Bork. Work in progress is also welcome!

Also have a look at the UnRAVeL seminar on Wednesdays (bi-weekly). And have a look at the Survey Lectures.

Upcoming Talks

Date	Speaker	Title	Where
	You?

Past Talks

Date	Speaker	Title
25.05.2021	Klara Nosan	On computing the Zariski closure of matrix groups
20.04.2021	Kevin Batz	Latticed k-Induction with an Application to Probabilistic Programs [Slides]
13.04.2021	Tobias Winkler	Model Checking Probabilistic Recursive Programs [Slides]
16.03.2021	Tim Quatmann	Multi-objective Optimization of Long-run Average and Total Rewards [Slides, Video (shortened)]
02.03.2021	Shahid Khan	Scalable Reliability Analysis by Lazy Verification
03.09.2020	Lutz Klinkenberg	Generating Functions for Probabilistic Programs
27.08.2020	Christopher Brix	Proving Non-Existence of Adversarial Examples in Deep Neural Networks using Symbolic Propagation with Error Bounds
20.08.2020	Shahid Khan	Initiators and all barriers algorithm for industry-scale BDMP analysis
06.08.2020	Joost-Pieter Katoen	Automated Termination Analysis of Polynomial Probabilistic Programs
30.07.2020	Alexander Hoppen	Probabilistic Programming IDE – A Feasibility Study [Slides]
23.07.2020	Bahare Salmani	Bayesian Inference by Symbolic Model Checking
09.07.2020	Marcin Szymczak	Towards efficient automated analysis of probabilistic programs [Slides]
25.06.2020	Tobias Winkler	Derived Automata and an Application to Markov Reward Chains [Slides]
Fronleichnam	Bas Westerbaan	A characterisation of ordered abstract probabilities (Bonus seminar)
28.05.2020	Kevin Batz	Towards an Expressive Assertion Language for Probabilistic Programs
14.05.2020	Jurriaan Rot	Learning Weighted Automata over Principal Ideal Domains [Slides]
30.04.2020	Philipp Berger	Benchmarking Software Model Checkers on Automotive Code [Slides]
16.04.2020	Mingshuai Chen	On ∞-Safety of Stochastic Differential Dynamics [Slides]

Past Past Talks

2019
	Hannah Mertens. Repairs in Dynamic Fault Trees: a Petri net semantics, Bachelor thesis presentation at RWTH Aachen University, 2019.
	Benjamin Lucien Kaminski. Advanced Weakest Precondition Calculi for Probabilistic Programs, Talk at PhD Defense, Aachen, 2019.
	Lukas Westhofen. Formal Verification of Industrial C Code, Master thesis presentation at RWTH Aachen University, 2019.
	Lyudmila Vatskicheva. Using Simulation to Improve the Precision of Hybrid Systems Reachability Analysis, Bachelor thesis presentation at RWTH Aachen University, 2019.
	Marwa Maghnie. Simulation and Optimization of Offshore Wind Farms, Master thesis presentation at RWTH Aachen University, 2019.
	Leon Rabanus. Solving Planning Problems with Success Probabilities Using SMT, Bachelor thesis presentation at RWTH Aachen University, 2019.
	Mahsa Shirmohammadi (CNRS & IRIF, France). On the Complexity of Value Iteration, Talk at RWTH Aachen University, 2019.
	Christoph Matheja. Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Pointer Programs, Talk at RWTH Aachen University, 2019.
	Thomas Ströder. Symbolic Execution and Program Synthesis: A General Methodology for Software Verification, PhD defense at RWTH Aachen University, 2019.
2018
	Christian Dehnert. The Probabilistic Model Checker Storm - Symbolic Methods for Probabilistic Model Checking, PhD defense at RWTH Aachen University, 2018.
	Dave Parker (University of Birmingham, UK). Verification and Strategy Synthesis for Stochastic Games, Talk at RWTH Aachen University, 2018.
	Fabian Meyer. A concept of expected size for an automated runtime analysis of probabilistic integer programs, Bachelor thesis presentation at RWTH Aachen University, 2018.
	Florian Frohn. Automated Complexity Analysis of Rewrite Systems, PhD defense at RWTH Aachen University, 2018.
	Ulrich Loup. On Solving Real-algebraic Formulas in a Satisfiability-modulo-theories Framework, PhD defense at RWTH Aachen University, 2018.
	Igor Bongartz. Explaining Unsolvable Planning Tasks with UNSAT Cores, Master thesis presentation at RWTH Aachen University, 2018.
	Alejandro Aguirre (IMDEA Software Institute, Spain). Almost Sure Productivity, Talk at RWTH Aachen University, 2018.
	Sebastian Arming (University of Salzburg, Austria). Parameter-Independent Strategies for pMDPs, Talk at RWTH Aachen University, 2018.
	Jiong Fu. Non-Termination Witnesses for C Programs, Master thesis presentation at RWTH Aachen University, 2018.
	Mahsa Varshosaz (Halmstad University, Sweden). Modeling and Model-Based Testing of Software product Lines, Talk at RWTH Aachen University, 2018.
	Tim Lange. IC3 Software Model Checking, PhD defense at RWTH Aachen University, 2018.
	Tom Neuhäuser. Quantifier Elimination by Cylindrical Algebraic Decomposition, Bachelor thesis presentation at RWTH Aachen University, 2018.
	Malte Neuß. Using Single CAD Cells as Explanations in MCSAT-style SMT Solving, Master thesis presentation at RWTH Aachen University, 2018.
	Ömer Sali. Linearization Techniques for Nonlinear Arithmetic Problems in SMT, Master thesis presentation at RWTH Aachen University, 2018.
	Mingshuai Chen (Institute of Software, Chinese Academy of Sciences, China). Modelling, Verification and Synthesis: A Peek into the Blueprint of Hybrid Systems, Talk at RWTH Aachen University, 2018.
	Thies Strothmann. Automated Complexity Analysis of Recursive Java Programs, Master thesis presentation at RWTH Aachen University, 2018.
	Nils Jonalik. kernDisc – Discovering Structure in Clinical Variable Data using Gaussian Processes, Bachelor thesis presentation at RWTH Aachen University, 2018.
	Alexander Bork. Analysing Dynamic Fault Trees by GSPNs, Bachelor thesis presentation at RWTH Aachen University, 2018.
	Harold Bruintjes. Model-Based Reliability Analysis of Aerospace Systems, PhD defense at RWTH Aachen University, 2018.
	Marcin Szymczak (University of Oxford, UK). Programming Language Semantics as a Foundation for Bayesian Inference, Talk at RWTH Aachen University, 2018.
	Sabrina Kowarsch. Modeling a Satellite with COMPASS, Master thesis presentation at RWTH Aachen University, 2018.
	Christopher Lösbrock. Implementing an Incremental Solver for Difference Logic, Bachelor thesis presentation at RWTH Aachen University, 2018.
	Fabian Schneider. A Unified Algebraic Shape Domain, Master thesis presentation at RWTH Aachen University, 2018.
	Lea Hiendl. Human-readable Scheduler Representation for Markov Decision Processes, Master thesis presentation at RWTH Aachen University, 2018.
	Marijn Heule (University of Texas, Austin, USA). Everything's Bigger in Texas: "The Largest Math Proof Ever", Talk at RWTH Aachen University, 2018.
	Ilias Kostireas (Wilfrid Laurier University, Waterloo, Ontario, Canada). Recent advances in the search for complementary sequences, Talk at RWTH Aachen University, 2018.
	Felix Bier. From Forest Automata to Hyperedge Replacement Grammars and Back, Master thesis presentation at RWTH Aachen University, 2018.
	Tim Quatmann. Multi-Cost Bounded Reachability in MDP, Talk at RWTH Aachen University, 2018.
	Lukas Netz. Analysis on Discretization of Gene Parameters in Evolutionary Algorithms, Master thesis presentation at RWTH Aachen University, 2018.
2017
	Joost-Pieter Katoen. Der deutsche Meister 2018 steht schon fest!?, Talk at RWTH Aachen University, 2017.
	Borzoo Bonakdarpour (McMaster University, Canada). Automated Fine-Tuning of Probabilistic Self-Stabilizing Algorithms, Talk at RWTH Aachen University, 2017.
	Matthijs Spaan (TU Delft, The Netherlands). Exploiting LP decomposition techniques for planning in Markov Decision Processes, Talk at RWTH Aachen University, 2017.
	Poornima Belavadi. Data Input and Processing in Model Based Risk Management for Medical Devices, Master thesis presentation at RWTH Aachen University, 2017.
	Predrag Filipovikj (Mälardalen University, Sweden). Pattern-based Specification and Formal Analysis of Embedded Systems Requirements and Behavioral Models, Talk at RWTH Aachen University, 2017.
	Anna Lukina (TU Wien, Austria). Resilient Control and Safety for Cyber-Physical Systems, Talk at RWTH Aachen University, 2017.
	Sven Deserno. Model Checking Markov Chain Families: Parameterised Structure and Probabilistic Reachability, Master thesis presentation at RWTH Aachen University, 2017.
	Feng Yijun (Peking University, China). CTMC model checking against multi-clock DTA specifications using PDE method, Talk at RWTH Aachen University, 2017.
	Sebastian Kruse. Model Checking a Wireless Token-Passing Protocol, Master thesis presentation at RWTH Aachen University, 2017.
	Leonard Korp. SMT-based planning for autonomous robot fleets, Bachelor thesis presentation at RWTH Aachen University, 2017.
	Hao Wu. Industrial Applications of Probabilistic Model Checking , Talk at RWTH Aachen University, 2017.
	Daniel Cloerkes. A Cyclic Proof System for Graph Grammar Inclusion, Bachelor thesis presentation at RWTH Aachen University, 2017.
	Tom Janson. Integrating Machine Learning and Model Checking for Model Repair, Talk at RWTH Aachen University, 2017.
	Tim Cramer. Analyzing Memory Accesses for Performance and Correctness of Parallel Programs, Talk at RWTH Aachen University, 2017.
	Arnd Hartmanns (University of Twente, The Netherlands). Time- and Reward-Bounded Probabilistic Model Checking Techniques, Talk at RWTH Aachen University, 2017.
	Mickael Randour (Université Libre de Bruxelles, Belgium). Rich behavioral models: illustration on journey planning and focus on multi- constraint percentile queries in Markov decision processes, Talk at RWTH Aachen University, 2017.
	Dustin Jungen. Repairs in Dynamic Fault Trees, Bachelor thesis presentation at RWTH Aachen University, 2017.
	Kevin Batz. Proof rules for expected runtimes of probabilistic programs, Bachelor thesis presentation at RWTH Aachen University, 2017.
	Tobias Heindel (University of Copenhagen, Denmark). Computing continuous-time Markov chains as transformers of unbounded observables, Talk at RWTH Aachen University, 2017.
	Ronja Nocon. Pattern based analysis of monotonicity on Dynamic Fault Trees, Bachelor thesis presentation at RWTH Aachen University, 2017.
	Michael Deutschen. Petri net semantics for Dynamic Fault Trees, Master thesis presentation at RWTH Aachen University, 2017.
	Ralf Wimmer (Albert-Ludwigs-Universität Freiburg). Solving dependency quantified Boolean Formulas, Talk at RWTH Aachen University, 2017.
	Nils Jansen (UT Austin, USA). Probabilistic Verification for Cognitive Models, Talk at RWTH Aachen University, 2017.
2016
	Hao Wu. Performance Evaluation on Modern Concurrent Data Structures, Talk at RWTH Aachen University, 2016.
	Philipp Berger. Game-based Abstraction of Parametric Markov Models, Master thesis presentation at RWTH Aachen University, 2016.
	Isabelle Tülleners. Graph-based Heap Abstraction for Balanced Data Structures, Bachelor thesis presentation at RWTH Aachen University, 2016.
	Christian Dehnert. Parameter Synthesis for Markov Models: Faster Than Ever, Talk at RWTH Aachen University, 2016.
	Christian Dehnert. Bounded Model Checking for Probabilistic Programs, Talk at RWTH Aachen University, 2016.
	Tim Quatmann. Multi-Objective Model Checking of Markov Automata, Master thesis presentation at RWTH Aachen University, 2016.
	Tom Janson. Accelerated Model Repair using Heuristic Analysis of Subsystems, Bachelor thesis presentation at RWTH Aachen University, 2016.
	Tim Lange. Introduction to IC3 and IC3CFA, Talk at RWTH Aachen University, 2016.
	Thomas Mertens. Efficient reuse of learnt information for control-flow oriented IC3 algorithms, Master thesis presentation at RWTH Aachen University, 2016.
	Frederick Prinz. Generalisation methods for control-flow oriented IC3 algorithms, Master thesis presentation at RWTH Aachen University, 2016.
	Matthias Volk. Advancing Dynamic Fault Tree Analysis, Talk at RWTH Aachen University, 2016.
	Florian Frohn. Automated Inference of Upper Complexity Bounds for Java Programs, Talk at RWTH Aachen University, 2016.
	Louis Wachtmeister. Analysing Cryptographically-Masked Information Flows Using Slicing, Bachelor thesis presentation at RWTH Aachen University, 2016.
	Matthias Naaf. Lower Runtime Bounds for Integer Programs, Talk at RWTH Aachen University, 2016.
	Alexander Hoppen. Non-Termination Analysis of LLVM IR Using Lassos, Bachelor thesis presentation at RWTH Aachen University, 2016.
	Joost-Pieter Katoen. The Satisfiability of Some Simple Probabilistic Logics, Talk at RWTH Aachen University, 2016.
	Federico Olmedo. Reasoning about Recursive Probabilistic Programs, Talk at RWTH Aachen University, 2016.
	Sebastian Junges. Uncovering Dynamic Fault Trees, Talk at RWTH Aachen University, 2016.
	Florian Frohn. Lower Runtime Bounds for Integer Programs, Talk at RWTH Aachen University, 2016.
	Matthias Volk. Advancing Dynamic Fault Tree Analysis, Talk at RWTH Aachen University, 2016.
	Felix Frei. Acyclicity Analysis for Java, Bachelor thesis presentation at RWTH Aachen University, 2016.
	Jens Katelaan (TU Wien, Austria). Logical Reasoning about Dynamic Memory: A Survey, Talk at RWTH Aachen University, 2016.
	Lijun Zhang (ISCAS, China). A Simple Algorithm for Solving Qualitative Probabilistic Parity Games, Talk at RWTH Aachen University, 2016.
	Johannes Hölzl (TU München). Markov chains and Markov decision processes in Isabelle/HOL, Talk at RWTH Aachen University, 2016.
	Hanna Franzen. Graph-Based Symbolic Execution for Pointer Programs with Data, Bachelor thesis presentation at RWTH Aachen University, 2016.
	Simon Froitzheim. Efficient Conversion of Geometric State Set Representations for Hybrid Systems, Bachelor thesis presentation at RWTH Aachen University, 2016.
	Fortunat Rajaona (University of Stellenbosch, South Africa). Program refinement and epistemic logic for reasoning about knowledge and privacy in multi-agents systems, Talk at RWTH Aachen University, 2016.
	Eric Heder. Design and implementation of a BDD-based planner for the assembly sequence planner in the field of the human-robot cooperation, Master thesis presentation at RWTH Aachen University, 2016.
	Dennis Guck (University of Twente, The Netherlands). Exploring Model Conformance Relations for the next airborne collision avoidance system (ACAS X), Talk at RWTH Aachen University, 2016.
	Enno Ruijters (University of Twente, The Netherlands). Fault maintenance trees and their application: Reliability-centered maintenance via stochastic model checking, Talk at RWTH Aachen University, 2016.
	Simon Feiden. Extending Probability Generating Function Semantics to Negative Variable Valuations, Bachelor thesis presentation at RWTH Aachen University, 2016.
	Hao Wu. Probabilistic Model Checking for Uncertain Scenario-Aware Data Flow, Talk at RWTH Aachen University, 2016.
	Hannah Arndt. Heap Abstraction Beyond Context-Freeness, Bachelor thesis presentation at RWTH Aachen Univeristy, 2016.
	Thies Strothmann. Termination Analysis for Concurrent Java Programs, Bachelor thesis presentation at RWTH Aachen University, 2016.
	Raoul Schaffranek. Modelling a purely functional subset of ECMAScript 2015, Bachelor thesis presentation at RWTH Aachen University, 2016.
	Benjamin Lucien Kaminski. Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs, Talk at RWTH Aachen University, 2016.
	Rebecca Haehn. Learning Control Strategies for Hybrid Vehicles using Neural Networks, Bachelor thesis presentation at RWTH Aachen University, 2016.
	David Korzeniewski. McMillan Prefixes for Stochastic Petri Nets, Master thesis presentation at RWTH Aachen University, 2016.
	Igor Bongartz. Over-approximative Reduction of Polytopes in the Context of Hybrid Systems Reachability Analysis, Bachelor thesis presentation at RWTH Aachen University, 2016.
	Christoph Matheja. Compositional Refinement of Separation Logic with Recursive Definitions, Talk at Winter colloquium Kleinwalsertal, 2016.
2015
	Christoph Matheja. Tree-Like Grammars and Separation Logic, Talk at RWTH Aachen University, 2015.
2014
	Thomas Mertens. Optimisation of Model Checking by Large Block Encoding, Bachelor thesis talk at RWTH Aachen University, 2014.