43 citations · 96 across the 13 of their papers we have counts for
Showing 2020Show all
2 papers · 1 filter
cs.LO2020
Relatively Complete Verification of Probabilistic Programs
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen +1
We study a syntax for specifying quantitative "assertions" - functions mapping program states to numbers - for probabilistic program verification. We prove that our syntax is expre…
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…