A formal approach to probabilistic termination
From MaRDI portal
(Redirected from A formal approach to probabilistic termination)
Recommendations
- Probabilistic termination: soundness, completeness, and compositionality
- Verification of Probabilistic Programs
- An abstract analysis of the probabilistic termination of programs
- New approaches for almost-sure termination of probabilistic programs
- Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs
Cited in
(41)- Using theorem proving to verify expectation and variance for discrete random variables
- Performance analysis and functional verification of the stop-and-wait protocol in HOL
- Verification of the Miller-Rabin probabilistic primality test.
- Markov chains and Markov decision processes in Isabelle/HOL
- Generating functions for probabilistic programs
- CryptHOL: game-based proofs in higher-order logic
- Algorithmic probabilistic game semantics. Playing games with automata
- Formal security proofs with minimal fuss: implicit computational complexity at work
- On the formalization of gamma function in HOL
- Formal reasoning about finite-state discrete-time Markov chains in HOL
- Probabilistic guarded commands mechanized in HOL
- Weakest precondition reasoning for expected run-times of probabilistic programs
- Probabilistic functions and cryptographic oracles in higher order logic
- Formal dependability modeling and analysis: a survey
- Probabilistic termination: soundness, completeness, and compositionality
- Formalising Semantics for Expected Running Time of Probabilistic Programs
- Probabilistic termination by monadic affine sized typing
- Three chapters of measure theory in Isabelle/HOL
- Liveness Reasoning with Isabelle/HOL
- Towards Formal Fault Tree Analysis Using Theorem Proving
- Formal Probabilistic Analysis of Stuck-at Faults in Reconfigurable Memory Arrays
- Formal verification of tail distribution bounds in the HOL theorem prover
- A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq
- scientific article; zbMATH DE number 4076588 (Why is no real title available?)
- scientific article; zbMATH DE number 2013585 (Why is no real title available?)
- An abstract analysis of the probabilistic termination of programs
- A Calculus for Game-Based Security Proofs
- Stochastic invariants for probabilistic termination
- Probabilistic_While
- Reasoning about conditional probabilities in a higher-order-logic theorem prover
- Towards the formal reliability analysis of oil and gas pipelines
- Verified analysis of random binary tree structures
- Measure construction by extension in dependent type theory with application to integration
- The probabilistic termination tool amber
- New approaches for almost-sure termination of probabilistic programs
- Generating counterexamples for quantitative safety specifications in probabilistic B
- Formal probabilistic analysis of detection properties in wireless sensor networks
- Proofs of randomized algorithms in Coq
- Using probabilistic Kleene algebra pKA for protocol verification
- Algebraic reasoning for probabilistic action systems and while-loops
- Formalization of the standard uniform random variable
This page was built for publication: A formal approach to probabilistic termination
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4484343)
