- phisch at cs.rwth-aachen.de
- Address
- Room 4230
Ahornstraße 55
D-52074 Aachen - Phone
- +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.
Quick Links
- Caesar, our deductive verifier for probabilistic programs
- Teaching
- 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 has been funded by the ERC Proof of Concept Grant VERIPROB, the ERC Advanced Grant FRAPPANT, and the 2022 WhatsApp Privacy Aware Program Analysis research award.
Teaching
Winter Semester 2024/25
Past Semesters
- SS24: Lecture Probabilistic Programming
- WS23/24: Lecture Concurrency Theory
- WS23/24: Seminar Deductive Verification
- 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
Selected Talks
- Dafny 2024: Caesar: A Verifier for Probabilistic Programs (link to video recording)
- VeriProP 2022: A Quantitative Verification Infrastructure
Peer Review
- FM 2024 (external reviewer)
- ECOOP 2024 (PC member Artifact Evaluation, rounds 1 and 2)
- OOPSLA 2024 (PC member Artifact Evaluation, rounds 1 and 2)
- 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)
Publications
A full list of publications is available on my ORCID profile, on my dblp profile, and on my Google Scholar profile.
| 2025 | |
|---|---|
[bibtex]
[issue]
|
Philipp Schröer, , , . Symbolic Quantitative Information Flow for Probabilistic Programs, Volume 15260 of LNCS, 128-154, Springer, 2025. |
| 2024 | |
[bibtex]
[issue]
|
Philipp Schroer. A deductive verifier for probabilistic programs, Master Thesis, RWTH Aachen University, 1 Online-Ressource: Illustrationen, RWTH Aachen University, 2024. |
| Show all | |