Philipp Schroer

Email
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

  1. Caesar, our deductive verifier for probabilistic programs
  2. Teaching
  3. Selected Talks
  4. Peer Review
  5. 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. The full list of Caesar-related publications can be found here.

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.

Website

Paper (extended version)

Github Repository

News

Teaching

Summer Semester 2026

Past Semesters

Selected Talks

Peer Review

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.

Publications

2026
DOIPhilipp Schroer, Joost-Pieter Katoen. Highly Incremental: A Simple Programmatic Approach for Many Objectives (Extended Version), 46 Seiten, 2026.
DOIPhilipp Schroer, Joost-Pieter Katoen. Highly Incremental: A Simple Programmatic Approach for Many Objectives, Formal methods : 27th international symposium, FM 2026, tokyo, japan, may 18–22, 2026, proceedings, part I / edited by augusto sampaio, marielle stoelinga, 559-577, Springer Nature Switzerland, 2026.
2025
DOIPhilipp Schroer, Francesca Randone, Raúl Pardo, Andrzej Wa̧sowski. Symbolic Quantitative Information Flow for Probabilistic Programs, Principles of verification: cycling the probabilistic landscape, part 1 / nils jansen, sebastian junges, benjamin lucien kaminski, christoph matheja, thomas noll, tim quatmann, mariëlle stoelinga, matthias volk, editors, 128-154, Springer, 2025.
DOIPhilipp Schroer, Darion Haase, Joost-Pieter Katoen. Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing (Extended Version), 2025.
2024
DOIPhilipp Schroer. A deductive verifier for probabilistic programs, 1 Online-Ressource: Illustrationen, RWTH Aachen University, 2024.
2023
DOIPhilipp Schroer, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. A Deductive Verification Infrastructure for Probabilistic Programs, 294, ACM, 2023.
DOIPhilipp Schroer, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. A Deductive Verification Infrastructure for Probabilistic Programs (Extended Version), [1]-48, 2023.
2020
DOIKevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schroer. PrIC3: Property Directed Reachability for MDPs, 2020.