Maximilian Schwenger

News

• Our paper “RTLola on Board: Testing Real Driving Emissions on your Phone” was accepted for TACAS’21! Find out more about it here.
• Our paper “Robust Monitoring for Medical Cyber-Physical Systems” was accepted for MedCPS@CPSWeek! Find out more about it here.
• Our papers “Verified Rust Monitors for Lola Specifications” (link), “Monitoring Cyber-Physical Systems: From Design to Integration” (link"), and “Automatic Optimizations for Stream-based Monitoring Languages” (link) were accepted for RV’20! Feel free to check them out.

Research Interests

• Runtime Verification
  Rarely are safety-critical systems sufficiently simple to be verified statically. So rather than verifying the correctness of all traces, testing validates the system on a select set of presumably-relevant executions. Runtime verification goes one step further: It keeps a close eye on the running system and thus verifies a single trace. This trace is by its nature highly relevant. Upon observation of undesired behavior, mitigation procedures can be initiated.
  
• Cyber-Physical Systems
  The interaction of a computer system with physical processes is a clash of two worlds: a computer works in a clocked, discrete world with clear semantics. When the processor’s clock rises, the internal state changes, when it falls, the world stands still. The real, physical world, however, is chaotic: nature does not wait for a clock tick to apply changes. Yet, the interaction of machines with the real world is essential: machines control power plants, cars, satellites and factories. So assisting the development process and finding suitable abstractions is a task worth pursuing.
  
• Synthesis
  Development for safety-critical software roughly follows the following pattern: assess requirements, formalize them, develop software complying to the requirements by hand, automatically verify them against the formal specification. If the verification fails, refine the software. Formal program synthesis aims at simplifying this process: assess requirements, formalize them, automatically synthesize a program that complies with the requirements by construction.

Publications

[FKSS21]	Robust Monitoring for Medical Cyber-Physical Systems. Joint work with Bernd Finkbeiner, Andreas Keller, and Jessica Schmidt. MedCPS@CPSWeek 2021. May 2021.
[BFKOPS21]	Automatic Optimizations for Runtime Verification Specifications. Joint work with Jan Baumeister, Bernd Finkbeiner, Matthis Kruse, Stefan Oswald and Noemi Passing. MT@CPSWeek 2021. May 2021.
[BFH+21]	RTLola on Board: Testing Real Driving Emissions on your Phone. Joint work with Sebastian Biewer, Bernd Finkbeiner, Holger Hermanns, Maximilian Köhl, and Yannik Schnitzer. TACAS 2021. March 2021.
[FOPS20]	Verified Rust Monitors for Lola Specifications. Joint work with Bernd Finkbeiner, Stefan Oswald and Noemi Passing. RV 2020. October 2020. Slides.
[S20]	Monitoring Cyber-Physical Systems: From Design to Integration. Tutorial Paper. RV 2020. October 2020. Slides.
[BFKS20]	Automatic Optimizations for Stream-based Monitoring Languages. Joint work with Jan Baumeister, Bernd Finkbeiner and Matthis Kruse. RV 2020. October 2020.
[BFSST20]	RTLola Cleared for Take-Off: Monitoring Autonomous Aircraft. Joint work with Jan Baumeister, Bernd Finkbeiner, Sebastian Schirmer and Christoph Torens. CAV 2020. July 2020.
[FSS20]	Simplex Architecture Meets RTLola. Joint work with Bernd Finkbeiner and Jessica Schmidt. MT@CPSWeek 2020. April 2020.
[MNS+20]	From LTL to rLTL Monitoring: Improved Monitorability through Robust Semantics. Joint work with Corto Mascle, Daniel Neider, Paulo Tabuada, Alexander Weinert, and Martin Zimmermann. HSCC 2020. April 2020. Slides, Technical Report
[S19]	Let’s not Trust Experience Blindly: Formal Monitoring of Humans and other CPS. Master Thesis at Saarland University. September 2019. Slides
[BFST19a]	FPGA Stream-Monitoring of Real-time Properties. Joint work with Jan Baumeister, Bernd Finkbeiner, and Hazem Torfah. EMSOFT 2019. October 2019. Slides.
[BFST19b]	On the Similarities of Aircraft and Humans: Monitoring CPS with StreamLAB. Joint work with Jan Baumeister, Bernd Finkbeiner, and Hazem Torfah. CyberCardia@ESWeek 2019. October 2019.
[FFS+19b]	StreamLAB: Stream-based Monitoring of Cyber-physical Systems. Joint work with Peter Faymonville, Bernd Finkbeiner, Malte Schledjewski, Marvin Stenger, Leander Tentrup and Hazem Torfah. CAV 2019. July 2019. Slides.
[FFS+19a]	Real-time Stream Monitoring with StreamLAB. Joint work with Peter Faymonville, Bernd Finkbeiner, Malte Schledjewski, Leander Tentrup and Hazem Torfah. MT@CPSWeek 2019. March 2019. Slides.
[STH+16]	From OpenCCG to AI Planning: Detecting Infeasible Edges in Sentence Generation. Joint work with Álvaro Torralba, Jörg Hoffmann, David Howcroft, and Vera Demberg, COLING 2016. December 2016.
[Schw16]	When a Sentece Falls apart. Using Heuristically Guided Dead End Detection in Natural Language Processing. Bachelor Thesis at Saarland University. December 2016.

Tools

LolaDrives	Android App for monitoring the emission of your car using RTLola
RTLola	Real-Time Stream Monitoring Framework
RustTyC	Type Checker Library written in Rust
rLTL Monitor	Monitor Construction for Robust LTL

Presentations

• Robust Monitoring for Medical Cyber-Physical Systems: Slides, Paper
  Workshop Talk at MedCPS 2021, May 2021.

• Verified Rust Monitors for Lola Specifications: Slides, Paper
  Conference Talk at RV 2020, October 2020.

• Monitoring Cyber-Physical Systems: From Design to Integration: Slides, Paper
  Tutorial at RV 2020, October 2020.

• From LTL to rLTL Monitoring: Slides, Paper
  Conference Talk at HSCC 2020, April 2020.

• Nobody’s Perfect: Monitoring Systems that Work Most of the Time: Slides
  Invited Talk at Toyota Research Institute, Boston, October 2019.

• Let’s not Trust Experience Blindly: Formal Runtime Verification for CPS: Slides
  Invited Talk at New York University and Yale University, October 2019.

• FPGA Stream-Monitoring of Real-time Properties: Slides, Paper
  Conference Talk at EMSOFT 2019, New York, October 2019.

• Let’s not Trust Experience Blindly: Formal Monitoring of Humans and other CPS: Slides
  Master Thesis Talk at Saarland University, August 2019

• StreamLAB: Stream-based Monitoring of Cyber-Physical Systems: Slides, Paper
  Conference Talk at CAV 2019, New York, July 2019.

• Real-time Stream Monitoring with StreamLAB: Slides, Paper
  Workshop Talk at MT@CPSWeek 2019. Montreal, April 2019

• XMas 4.0 Digitalisierung am Nordpol Slides (de), (en)
  Christmas Lecture for 24h Lecture, Saarland University, December 2017

• Real-Time Stream Monitoring Slides, Paper
  Qualifying Exam at Saarland University, May 2017

Research Assistants

• Stefan Oswald
  Static Analyses for RTLola Specifications, 2021 ongoing
• Jessica Schmidt
  Robust Runtime Verification, 2021
• Florian Kohn
  Network Runtime Verification, 2019 – 2021
• Sanny Schmitt
  Learning Hybrid Automata, 2019 – 2020
• Rafael Dewes
  Synthesis of Autonomous Robots, 2019
• Daniel Schäfer
  Synthesis of Autonomous Robots, 2019
• Jan Baumeister
  Translating RTLola Specifications to FPGA, 2018 – 2019
  Check out the EMSOFT’19 Paper!

Advised Theses

• Stefan Oswald: Model-Refinement via Runtime Monitoring
  Master Thesis, ongoing
• Leonard Niemann: Outlier Prediction in Image Streams
  Bachelor Thesis, ongoing
• Rafael Dewes: Monitoring HyperMTL
  Master Thesis
• Jessica Schmidt: Robust Runtime Verification for Medical CPS
  Bachelor Thesis, 2021
  Check out the MCPS’21 Workshop Paper!
• Carsten Gerstacker: Specification-Aided Trajectory Prediction with Recurrent Neural Networks
  Master Thesis, 2020
• Stefan Oswald: Verifiable Runtime Monitor Generation for Lola Specifications
  Bachelor Thesis, 2020; Co-advised by Noemi Passing
  Check out the RV’20 Paper!
• Daniel Schäfer: Synthesizing Epistemic Specifications Using LTL Synthesis Tools
  Master Thesis, 2020
• Jan Baumeister: Tracing Correctness: A Practical Approach to Traceable Runtime Monitoring
  Master Thesis, 2020
  Check out the CAV’20 Paper!
• Paul Bungert: Monitoring Hybrid Automata
  Bachelor Thesis, 2019
• Hendrik Leidinger: Learning the Desired Behavior for Causality Analyses
  Master Thesis, 2019
• Christoph Rosenhauer: Compiling Lola 2.0 to C
  Bachelor Thesis, 2019
• Marvin Hofmann: Runtime Verification of Critical Web-based Systems
  Bachelor Thesis, 2018
• Lukas Stemmler: Communication Rules for Static Networks
  Bachelor Thesis 2018

Scientific Service

• RV’21 (Reviewer)
• CONCUR’21 (Reviewer)
• CAV’21 (Reviewer)
• ICTAC’20 (Reviewer)
• RV’20 (Reviewer)
• CONCUR’20 (Reviewer)
• NASA FM’20 (Reviewer)
• CSL’20 (Reviewer)

(Mostly) Useful References

How to Write Well	Compilation of Common Mistakes
How to Write Papers so People Can Read Them	Slides by Derek Dreyer
On Preparing Good Talks	Slides by Ranjit Jhala
My Personal Github	Thesis Template, Keyboard Layout for CS People, etc.
Saarlandian Rust Meetup	Lecture Series introducing the Rust Programming Language by Andreas Schmidt, Florian Fromm, and myself. Check out my slides on Functional Programming and Structs.

Teaching

Summer 2021	Assistant for Monitoring of Cyber-Physical Systems
Summer 2019	Assistant for Hybrid Systems
Summer 2018	Assistant for Embedded Systems
Winter 2017	Assistant for Time Machine
Summer 2017	Coach for Mathematics Precourse
Winter 2016	Tutor for Verification at the Reactive Systems Group
Summer 2016	Student Tutor for Embedded Systems at the Reactive Systems Group
Summer 2015	Tutor for Artificial Intelligence at the Foundations of Artificial Intelligence Group
Winter 2014	Tutor for Theoretical Computer Science at the Computational Complexity Group
Summer 2014	Tutor for System Architecture at the Real-Time and Embedded Systems Lab