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)
9 Pith papers cite this work. Polarity classification is still indexing.
9
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.
Introduces parametric Markov Automata and a two-step discretization approach to pMDPs that computes bounds on time-bounded reachability probabilities up to arbitrary precision.
UMB is a new binary file format for probabilistic systems that provides a unified, efficient alternative to tool-specific textual representations.
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
-
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.