3 papers
cs.PL2026
Towards a Deductive Verification Infrastructure for Weighted Programming
Emma Ahrens, Samuel Rode, Philipp Schröer +1
Weighted programs extend guarded commands with trace weights drawn from a semiring, or more generally a monoid-module. Varying this algebra gives one programmatic syntax for a vari…
cs.PL2025
Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing (Extended Version)
Philipp Schröer, Darion Haase, Joost-Pieter Katoen
This paper focuses on effective user diagnostics generated during the deductive verification of probabilistic programs. Our key principle is based on providing slices for (1) error…
cs.LO2020
PrIC3: Property Directed Reachability for MDPs
Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski +3
IC3 has been a leap forward in symbolic model checking. This paper proposes PrIC3 (pronounced pricy-three), a conservative extension of IC3 to symbolic model checking of MDPs. Our…