works on

From the 1 of 12 linked papers with an AI index.

activity
20242026
collaborators
Showing cs.PLShow all

5 papers · 1 filter

cs.PL2026

A Fast Quantitative Analyzer for NetKAT

Thomas Lu, Qiancheng Fu, Kevin Batz +5

The paper introduces a fast analyzer for quantitative network properties using weighted NetKAT, employing a symbolic data structure and specialized algorithms to efficiently comput…

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…

cs.PL20261 cited

Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops (Extended Version)

Darion Haase, Kevin Batz, Adrian Gallus +4

A fundamental computational task in probabilistic programming is to infer a program's output (posterior) distribution from a given initial (prior) distribution. This problem is cha…