scientific article; zbMATH DE number 1927425
From MaRDI portal
Publication:4484343
zbMATH Open1013.68193MaRDI QIDQ4484343FDOQ4484343
Authors: Joe Hurd
Publication date: 12 June 2003
Full work available at URL: http://link.springer.de/link/service/series/0558/bibs/2410/24100230.htm
Title of this publication is not available (Why is that?)
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)
- Liveness Reasoning with Isabelle/HOL
- Title not available (Why is that?)
- The probabilistic termination tool amber
- Weakest precondition reasoning for expected run-times of probabilistic programs
- Probabilistic termination by monadic affine sized typing
- Reasoning about conditional probabilities in a higher-order-logic theorem prover
- Formalising Semantics for Expected Running Time of Probabilistic Programs
- Generating functions for probabilistic programs
- Formal dependability modeling and analysis: a survey
- Title not available (Why is that?)
- Performance analysis and functional verification of the stop-and-wait protocol in HOL
- New approaches for almost-sure termination of probabilistic programs
- Measure construction by extension in dependent type theory with application to integration
- Towards Formal Fault Tree Analysis Using Theorem Proving
- Verification of the Miller-Rabin probabilistic primality test.
- Formalization of the standard uniform random variable
- Probabilistic termination: soundness, completeness, and compositionality
- Using probabilistic Kleene algebra pKA for protocol verification
- CryptHOL: game-based proofs in higher-order logic
- A Calculus for Game-Based Security Proofs
- Formal security proofs with minimal fuss: implicit computational complexity at work
- Verified analysis of random binary tree structures
- Proofs of randomized algorithms in Coq
- A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq
- Formal probabilistic analysis of detection properties in wireless sensor networks
- Using theorem proving to verify expectation and variance for discrete random variables
- Formal Probabilistic Analysis of Stuck-at Faults in Reconfigurable Memory Arrays
- Algorithmic probabilistic game semantics. Playing games with automata
- On the formalization of gamma function in HOL
- Formal reasoning about finite-state discrete-time Markov chains in HOL
- Formal verification of tail distribution bounds in the HOL theorem prover
- Probabilistic functions and cryptographic oracles in higher order logic
- Generating counterexamples for quantitative safety specifications in probabilistic B
- Probabilistic guarded commands mechanized in HOL
- Algebraic reasoning for probabilistic action systems and while-loops
- Markov chains and Markov decision processes in Isabelle/HOL
- Three chapters of measure theory in Isabelle/HOL
- Towards the formal reliability analysis of oil and gas pipelines
- Title not available (Why is that?)
- Stochastic invariants for probabilistic termination
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)