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.

        Funding. The project is funded by our ERC Advanced Grant FRAPPANT and the 2022 WhatsApp Privacy Aware Program Analysis research award.

        Website
        Paper (extended version)
        Github Repository

        Teaching

        Current Semester

        Past Semesters

        Selected Talks

        • Dafny 2024: Caesar: A Verifier for Probabilistic Programs (upcoming)
        • VeriProP 2022: A Quantitative Verification Infrastructure

        Peer Review

        • 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 list of publications is also available on my ORCID profile, on my dblp profile, and on my Google Scholar profile.

        2023
        DOI fulltext PDF [bibtex]
        @article{ADVIPP2023,
        title = {A Deductive Verification Infrastructure for Probabilistic Programs},
        author = {Philipp Schroer and Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
        publisher = {ACM},
        journal = {Proceedings of the ACM on programming languages},
        volume = {7(OOPSLA2)},
        pages = {pages 294},
        type = {Journal Article},
        year = {2023},
        doi = {10.1145/3622870},
        url = { https://publications.rwth-aachen.de/record/973293},
        }×
        [issue]         		Philipp Schroer, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. A Deductive Verification Infrastructure for Probabilistic Programs, Proceedings of the ACM on programming languages 7 (OOPSLA2), pages 294, ACM, 2023.
        DOI arXiv:2309.07781 fulltext PDF [bibtex]
        @unpublished{ADVIPPEV2023,
        title = {A Deductive Verification Infrastructure for Probabilistic Programs (Extended Version)},
        author = {Philipp Schroer and Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
        pages = {[1]-48},
        type = {Preprint},
        year = {2023},
        doi = {10.48550/arXiv.2309.07781},
        url = { https://arxiv.org/abs/2309.07781},
        }×
        [issue]         		Philipp Schroer, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. A Deductive Verification Infrastructure for Probabilistic Programs (Extended Version), [1]-48, 2023. https://arxiv.org/abs/2309.07781
        2021
        DOI fulltext PDF [bibtex]
        @conference{LIAPP2021,
        title = {Latticed $k$-Induction with an Application to Probabilistic Programs},
        author = {Kevin Batz and Mingshuai Chen and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Philipp Schröer},
        publisher = {Springer},
        booktitle = {LNCS},
        volume = {12760},
        pages = {524-549},
        type = {Conference Paper},
        year = {2021},
        doi = {10.1007/978-3-030-81688-9_25},
        url = { https://publications.rwth-aachen.de/record/822587},
        }×
        [issue]         		Kevin Batz, Mingshuai Chen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, 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.
        Show all