- phisch at cs.rwth-aachen.de
- Room 4230
- +49 241 80 21222
I am a PhD student in the Software Modeling and Verification Group headed by Professor J.-P. Katoen. On some publications, my last name is spelt Schröer (with an “ö”).
Research. My research interests include probabilistic programs and their automated verification. I am mainly working on a deductive verification infrastructure and an intermediate verification language for probabilistic programs (see below).
Communication. I speak German and English. Please call me Philipp and address me as “Du” in German. 🙂 If I don’t respond to your email within two days, don’t hesitate to send a follow-up email.
- Caesar, our deductive verifier for probabilistic programs
- Selected Talks
- Peer Review
- Publications – (dblp profile, Google Scholar profile)
A Deductive Verification Infrastructure for Probabilistic Programs
Overview. We are developing Caesar, a deductive verifier for probabilistic programs. It is based on our verification infrastructure for probabilistic programs, similar to a probabilistic version of Boogie. Our work includes an intermediate verification language called HeyVL and a real-valued logic called HeyLo. This allows us to generate verification conditions that prove a program’s correctness. Our focus is on measuring properties like expected outcomes and termination probabilities, so we use a real-valued approach instead of the usual Boolean logic. Our IVL adapts standard verification elements to handle quantitative aspects and uses weakest preexpectation-style semantics to generate verification conditions. Our SMT-based implementation Caesar enables us to automatically verify a wide range of benchmarks.
Publications. Caesar has a website where you can download the tool and find its documentation, including a tutorial-style guide. It is developed as an open-source project on Github. A paper on HeyVL and Caesar was published at OOPSLA 2023 and there’s an extended version available on arxiv. The artifact submitted to OOPSLA 2023 received the Distinguished Artifact award.
Funding. The project is funded by our ERC Advanced Grant FRAPPANT and the 2022 WhatsApp Privacy Aware Program Analysis research award.
- SS23: Lecture Semantics and Verification of Software
- SS23: Seminar Probabilistic Programming
- WS22/23: Lecture Probabilistic Programming
- WS22/23: Seminar Probabilistic Programming
- SS22: Seminar Trends in Computer-Aided Verification
- Dafny 2024: Caesar: A Verifier for Probabilistic Programs (upcoming)
- VeriProP 2022: A Quantitative Verification Infrastructure
- TACAS 2023 (external reviewer)
- QEST 2023 (PC member Artifact Evaluation)
- CAV 2022 (PC member Artifact Evaluation)
- POPL 2022 (PC member Artifact Evaluation)
- CAV 2021 (PC member Artifact Evaluation)
|[bibtex] [issue]||Philipp Schroer, Kevin Batz, , Joost-Pieter Katoen, . A Deductive Verification Infrastructure for Probabilistic Programs, Proceedings of the ACM on programming languages 7 (OOPSLA2), pages 294, ACM, 2023.|
|[bibtex] [issue]||Philipp Schroer, Kevin Batz, , Joost-Pieter Katoen, . A Deductive Verification Infrastructure for Probabilistic Programs (Extended Version), -48, 2023. https://arxiv.org/abs/2309.07781|
|[bibtex] [issue]||Kevin Batz, Mingshuai Chen, , Joost-Pieter Katoen, , Philipp Schröer. Latticed $k$-Induction with an Application to Probabilistic Programs, 33. International Conference on Computer-Aided Verification (CAV 2021), Volume 12760 of LNCS, 524-549, Springer, 2021.|