activity
20182026
most citedA Deductive Verification Infrastructure for Probabilistic Programs (Extended Version)

22 citations · 26 across the 11 of their papers we have counts for

collaborators
Showing cs.PLShow all

10 papers · 1 filter

cs.PL2026

Type-Directed Discretization of Probabilistic Programs (Extended Version)

Katherine Wu, Jules Jacobs, Kevin Batz +1

We study exact discretization as a semantics-preserving transformation for recursive, higher-order probabilistic programs with continuous distributions. We target programs where co…

cs.PL2026

Multiobjective Preexpectation Reasoning for Probabilistic Programs

Lena Verscht, Hannah Mertens, Kevin Batz +3

Probabilistic programs with nondeterminism model planning problems in which a strategy resolves the nondeterminism to optimize an expected outcome. We study the multiobjective sett…

cs.PL2026

A Fast Quantitative Analyzer for NetKAT

Thomas Lu, Qiancheng Fu, Kevin Batz +5

When designing a network, engineers must navigate trade-offs (e.g., one topology offers more aggregate bandwidth, another lower latency or better resilience) that demand reasoning…

cs.PL2026

Scalable Probabilistic Program Verification via Typed Extended Decision Diagrams

Daniel Basgöze, Kevin Batz, Sebastian Junges +1

Weakest pre-expectations are the probabilistic program analogue to weakest preconditions in classical programs. Deductive verification approaches aim to establish bounds on these q…

cs.PL2026

Caesar: A Deductive Verifier for Probabilistic Programs

Philipp Schröer, Kevin Batz, Umut Yiğit Dural +4

Caesar is a deductive verifier for probabilistic programs. At its core lies HeyVL, a quantitative intermediate verification language based on the real-valued logic HeyLo. HeyVL all…

cs.PL2026

Weighted NetKAT: A Programming Language For Quantitative Network Verification

Emmanuel Suárez Acevedo, Tiago Ferreira, Kevin Batz +3

We introduce weighted NetKAT, a domain-specific language for modeling and verifying quantitative network properties. The language is parametric on a semiring, enabling the treatmen…