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