I am a Ph.D. student in the Computer Science Department of Saarland University working at CISPA Helmholtz Center for Information Security.
I am also a member of the Graduate School of Computer Science.
|Reactive Systems Group|
|CISPA Helmholtz Center for Information Security|
|Building: E 1.1, Room: 1.08|
|Phone:||+49 681 302 5654|
|eMail:||maximilian.schwenger at cispa.de|
|Office Hours:||Whenever my door is open|
- 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.
- 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.
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.
|[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.
|[S20]||Monitoring Cyber-Physical Systems: From Design to Integration.
Tutorial Paper. RV 2020. October 2020.
|[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.
|[BFST19a]||FPGA Stream-Monitoring of Real-time Properties.
Joint work with Jan Baumeister, Bernd Finkbeiner, and Hazem Torfah. EMSOFT 2019. October 2019.
|[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.
|[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.
|[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.
|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|
- 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.
- 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
- 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!
- Stefan Oswald: Model-Refinement via Runtime Monitoring
Master Thesis, ongoing
- Leonard Niemann: Outlier Prediction in Image Streams
Bachelor Thesis, ongoing
- Rafael Dewes: Monitoring HyperMTL
- 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
- 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
||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.
|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|