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 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

        Winter Semester 2024/25

        Past Semesters

        Selected Talks

        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.


        Warning: SQLite3::prepare(): Unable to prepare statement: 5, database is locked in /var/www/html/inc/sqlite-access.php on line 428

        Fatal error: Uncaught SQLiteAccessException: Could not prepare statement: REPLACE INTO publications (pub_id, type_id, title, year, pages, publisher, institution, arxiv_id, doi_id, fulltext) VALUES (:pub_id, :type_id, :title, :year, :pages, :publisher, :institution, :arxiv_id, :doi_id, :fulltext); in /var/www/html/inc/sqlite-access.php:433 Stack trace: #0 /var/www/html/inc/sqlite-access.php(64): dbAccess->prepare('REPLACE INTO pu...') #1 /var/www/html/inc/sqlite-access.php(45): dbAccess->prepareStmts() #2 /var/www/html/index.php(73): dbAccess->__construct('/var/www/html/d...', 1) #3 {main} thrown in /var/www/html/inc/sqlite-access.php on line 433