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. |