Caesar introduces a deductive verifier for probabilistic programs using the HeyVL language, Z3 SMT solving, and a probabilistic model-checking backend after five years of development.
International Journal on Software Tools for Technology Transfer24(4), 589–610 (Aug 2022)
7 Pith papers cite this work. Polarity classification is still indexing.
7
Pith papers citing it
citation-role summary
background 1
citation-polarity summary
roles
background 1polarities
background 1representative citing papers
A new efficient algorithm computes optimal conditional reachability probabilities in MDPs without creating hard cyclic reductions, achieving linear time on acyclic cases and substantial speedups on benchmarks from Bayesian networks, probabilistic programs, and runtime monitoring.
New framework for probabilistic safety shields in MDPs showing impossibility of strong classical guarantees and providing weaker but usable alternatives with offline and online constructions.
In concurrent graph games with distributed private randomness, memoryless strategies decide threshold reachability (NP-hard) and almost-sure reachability is NP-complete; IRATL extends ATL for probability thresholds without shared randomness.
A POMDP decomposition method scales solving of the Sensor Selection Problem and Positional Observability Problem by 3 and 5 orders of magnitude in instance size and runtime.
Presents hierarchical adaptive refinement to accelerate near-optimal policy synthesis in MDPs up to 1M states with up to 2x speedup over PRISM and formal error bounds.
citing papers explorer
-
Caesar: A Deductive Verifier for Probabilistic Programs
Caesar introduces a deductive verifier for probabilistic programs using the HeyVL language, Z3 SMT solving, and a probabilistic model-checking backend after five years of development.
-
Fast Computation of Conditional Probabilities in MDPs and Markov Chain Families
A new efficient algorithm computes optimal conditional reachability probabilities in MDPs without creating hard cyclic reductions, achieving linear time on acyclic cases and substantial speedups on benchmarks from Bayesian networks, probabilistic programs, and runtime monitoring.
-
Shields to Guarantee Probabilistic Safety in MDPs
New framework for probabilistic safety shields in MDPs showing impossibility of strong classical guarantees and providing weaker but usable alternatives with offline and online constructions.
-
Randomise Alone, Reach as a Team
In concurrent graph games with distributed private randomness, memoryless strategies decide threshold reachability (NP-hard) and almost-sure reachability is NP-complete; IRATL extends ATL for probability thresholds without shared randomness.
-
Scaling Observation-aware Planning in Uncertain Domains
A POMDP decomposition method scales solving of the Sensor Selection Problem and Positional Observability Problem by 3 and 5 orders of magnitude in instance size and runtime.
-
Accelerating Policy Synthesis in Large-Scale MDPs via Hierarchical Adaptive Refinement
Presents hierarchical adaptive refinement to accelerate near-optimal policy synthesis in MDPs up to 1M states with up to 2x speedup over PRISM and formal error bounds.
- Extending QuAK with Nested Quantitative Automata