Latticed \(k\)-induction with an application to probabilistic programs (Q832288): Difference between revisions

@@ Property / arXiv ID @@
+.14100
@@ Property / arXiv ID: 2105.14100 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4843177
@@ Property / cites work: Q4843177 / rank @@
+Normal rank
@@ Property / cites work @@
+Ensuring the reliability of your model checker: interval iteration for Markov decision processes
+Normal rank
@@ Property / cites work @@
+Fixpoint theory -- upside down
@@ Property / cites work: Fixpoint theory -- upside down / rank @@
+Normal rank
@@ Property / cites work @@
+Synthesizing Probabilistic Invariants via Doob’s Decomposition
+Normal rank
@@ Property / cites work @@
+\textsf{PrIC3}: property directed reachability for MDPs
+Normal rank
@@ Property / cites work @@
+Latticed \(k\)-induction with an application to probabilistic programs
+Normal rank
@@ Property / cites work @@
+Q4817533
@@ Property / cites work: Q4817533 / rank @@
+Normal rank
@@ Property / cites work @@
+SAT-Based Model Checking without Unrolling
@@ Property / cites work: SAT-Based Model Checking without Unrolling / rank @@
+Normal rank
@@ Property / cites work @@
+A counterexample-guided abstraction-refinement framework for markov decision processes
+Normal rank
@@ Property / cites work @@
+Bounded model checking using satisfiability solving
+Normal rank
@@ Property / cites work @@
+Constructive versions of Tarski's fixed point theorems
+Normal rank
@@ Property / cites work @@
+Q4798031
@@ Property / cites work: Q4798031 / rank @@
+Normal rank
@@ Property / cites work @@
+Automatic analysis of DMA races using model checking and \(k\)-induction
+Normal rank
@@ Property / cites work @@
+Finding Polynomial Loop Invariants for Probabilistic Programs
+Normal rank
@@ Property / cites work @@
+Optimistic value iteration
@@ Property / cites work: Optimistic value iteration / rank @@
+Normal rank
@@ Property / cites work @@
+Q2849848
@@ Property / cites work: Q2849848 / rank @@
+Normal rank
@@ Property / cites work @@
+Bounded model checking for probabilistic programs
@@ Property / cites work: Bounded model checking for probabilistic programs / rank @@
+Normal rank
@@ Property / cites work @@
+Tools and Algorithms for the Construction and Analysis of Systems
+Normal rank
@@ Property / cites work @@
+On the hardness of analyzing probabilistic programs
+Normal rank
@@ Property / cites work @@
+Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms
+Normal rank
@@ Property / cites work @@
+Linear-Invariant Generation for Probabilistic Programs:
+Normal rank
@@ Property / cites work @@
+A probabilistic PDL
@@ Property / cites work: A probabilistic PDL / rank @@
+Normal rank
@@ Property / cites work @@
+Interpolating strong induction
@@ Property / cites work: Interpolating strong induction / rank @@
+Normal rank
@@ Property / cites work @@
+Randomized mutual exclusion algorithms revisited
@@ Property / cites work: Randomized mutual exclusion algorithms revisited / rank @@
+Normal rank
@@ Property / cites work @@
+Fixed point theorems and semantics: A folk tale
@@ Property / cites work: Fixed point theorems and semantics: A folk tale / rank @@
+Normal rank
@@ Property / cites work @@
+Abstraction, Refinement and Proof for Probabilistic Systems
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+An interpolating theorem prover
@@ Property / cites work: An interpolating theorem prover / rank @@
+Normal rank
@@ Property / cites work @@
+Inferring expected runtimes of probabilistic integer programs using expected sizes
+Normal rank
@@ Property / cites work @@
+Q3992568
@@ Property / cites work: Q3992568 / rank @@
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Q5624635
@@ Property / cites work: Q5624635 / rank @@
+Normal rank
@@ Property / cites work @@
+Complete Lattices and Up-To Techniques
@@ Property / cites work: Complete Lattices and Up-To Techniques / rank @@
+Normal rank
@@ Property / cites work @@
+Enhancements of the bisimulation proof method
@@ Property / cites work: Enhancements of the bisimulation proof method / rank @@
+Normal rank
@@ Property / cites work @@
+Sound value iteration
@@ Property / cites work: Sound value iteration / rank @@
+Normal rank
@@ Property / cites work @@
+Bounded model checking of infinite state systems
@@ Property / cites work: Bounded model checking of infinite state systems / rank @@
+Normal rank
@@ Property / cites work @@
+A lattice-theoretical fixpoint theorem and its applications
+Normal rank
@@ Property / cites work @@
+Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking
+Normal rank