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 Cleared for Take-Off: Monitoring Autonomous Aircraft” was accepted for CAV’20! Find out more about it here.
- My tutorial “Monitoring Cyber-Physical Systems: From Design to Integration” was accepted for RV’20! Check it out here.
- Our papers “Verified Rust Monitors for Lola Specifications” (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.
|[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.
- 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
|RustTyC||Type Checker Library written in Rust|
|RTLola||Real-Time Stream Monitoring Framework|
|rLTL Monitor||Monitor Construction for Robust LTL|
- Rafael Dewes: Master Thesis, ongoing
- Stefan Oswald: Research Assistant, ongoing
Static Analyses for RTLola Specifications
- Jessica Schmidt: Bachelor Thesis, ongoing
Robust Runtime Verification for Medical CPS
- Florian Kohn: Research Assistant, 2019 – ongoing
Network Runtime Verification
- Carsten Gerstacker: Master Thesis, 2020
Specification-Aided Trajectory Prediction with Recurrent Neural Networks
- Stefan Oswald: Bachelor Thesis, 2020
Verifiable Runtime Monitor Generation for Lola Specifications
Co-advised by Noemi Passing
- Daniel Schäfer: Master Thesis
Synthesizing Epistemic Specifications Using LTL Synthesis Tools (pdf coming soon)
- Sanny Schmitt: Research Assistant, 2019 – 2020
Learning Hybrid Automata
- Jan Baumeister: Master Thesis, 2020
Tracing Correctness: A Practical Approach to Traceable Runtime Monitoring
- Paul Bungert: Bachelor Thesis, 2019
Monitoring Hybrid Automata
- Rafael Dewes: Research Assistant, 2019
Synthesis of Autonomous Robots
- Daniel Schäfer: Research Assistant, 2019
Synthesis of Autonomous Robots
- Jan Baumeister: Research Assistant, 2018 – 2019
Translating RTLola Specifications to FPGA
- Hendrik Leidinger: Master Thesis, 2019
Learning the Desired Behavior for Causality Analyses
- Christoph Rosenhauer: Bachelor Thesis, 2019
Compiling Lola 2.0 to C
- Marvin Hofmann: Bachelor Thesis, 2018
Runtime Verification of Critical Web-based Systems
- Lukas Stemmler: Bachelor Thesis 2018
Communication Rules for Static Networks
- Reviewer for ICTAC’20
- Reviewer for RV’20
- Reviewer for CONCUR’20
- Reviewer for NASA FM’20
- Reviewer for CSL’20
(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 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|