Philipp Schroer
- phisch@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.
Caesar: A Deductive Verifier for Probabilistic Programs
We are developing Caesar, a deductive verifier for probabilistic programs. It proves quantitative properties such as bounds on expected values, expected runtimes, and termination probabilities.
Our verification infrastructure combines the intermediate verification language HeyVL with the real-valued logic HeyLo, serving a role similar to Boogie for quantitative verification. Caesar generates verification conditions using weakest preexpectation-style semantics and checks them with SMT solvers. The Caesar website provides downloads, documentation, and a tutorial-style guide.
Publications. Our foundational paper was published at OOPSLA 2023, with an extended version on arXiv. Its artifact received the Distinguished Artifact award. See the full list of Caesar-related publications for subsequent work.
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
Summer Semester 2026
Past Semesters
- WS25/26: Lecture Probabilistic Programming
- WS25/26: Practical Course Model Checking
- SS25: Practical Course Implementation of Heuristic Algorithms for Board Games
- WS24/25: Seminar Probabilistic Programming
- WS24/25: Practical Course Model Checking
- 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
- Caesar at Summer School for Formal Techniques ’25
- 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
There’s a list of publications about Caesar on its website.
A full list of my own publications is available on my ORCID profile, on my dblp profile, and on my Google Scholar profile.
Own publications
2026
- Conference paper
Highly Incremental: A Simple Programmatic Approach for Many Objectives
Formal Methods
- Preprint
Highly Incremental: A Simple Programmatic Approach for Many Objectives (Extended Version)
PDF of Highly Incremental: A Simple Programmatic Approach for Many Objectives (Extended Version)RWTH record for Highly Incremental: A Simple Programmatic Approach for Many Objectives (Extended Version)BibTeX for Highly Incremental: A Simple Programmatic Approach for Many Objectives (Extended Version) - Artifact
Zenodo
2025
- PreprintPDF of Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing (Extended Version)RWTH record for Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing (Extended Version)BibTeX for Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing (Extended Version)
- Book chapter
Symbolic Quantitative Information Flow for Probabilistic Programs
Principles of verification: cycling the probabilistic landscape, Part 1
2024
- Master’s thesis
A deductive verifier for probabilistic programs
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Peter Müller
Consultants: Kevin Batz, Benjamin Kaminski, Christoph Matheja
2023
- Journal article
A Deductive Verification Infrastructure for Probabilistic Programs
Proceedings of the ACM on programming languages
2021
- Conference paper
Latticed $k$-Induction with an Application to Probabilistic Programs
Computer-Aided Verification
2020
Supervised theses
2026
- Bachelor’s thesis
Integrating KoAT’s push-button probabilistic cost analysis into Caesar
RWTH Aachen University
Advisers: Jürgen Giesl, Tim Quatmann
Consultants: Philipp Schroer, Nils Michael Lommen
2025
- Master’s thesis
Effective quantifier-based reasoning for quantitative deductive verification
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Philipp Schroer, Darion Haase