scientific article; zbMATH DE number 1927425

From MaRDI portal

zbMath1013.68193MaRDI QIDQ4484343

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: zbMATH Open Web Interface contents unavailable due to conflicting licenses.



Related Items

Towards Formal Fault Tree Analysis Using Theorem Proving, Liveness Reasoning with Isabelle/HOL, CryptHOL: game-based proofs in higher-order logic, Measure construction by extension in dependent type theory with application to integration, Verification of the Miller-Rabin probabilistic primality test., Formal probabilistic analysis of detection properties in wireless sensor networks, Markov chains and Markov decision processes in Isabelle/HOL, Formal reasoning about finite-state discrete-time Markov chains in HOL, Generating counterexamples for quantitative safety specifications in probabilistic B, Proofs of randomized algorithms in Coq, Using probabilistic Kleene algebra pKA for protocol verification, Algebraic reasoning for probabilistic action systems and while-loops, Algorithmic probabilistic game semantics. Playing games with automata, Reasoning about conditional probabilities in a higher-order-logic theorem prover, A Calculus for Game-Based Security Proofs, Formal Probabilistic Analysis of Stuck-at Faults in Reconfigurable Memory Arrays, Formal verification of tail distribution bounds in the HOL theorem prover, Formalization of the standard uniform random variable, Verified analysis of random binary tree structures, 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, Three Chapters of Measure Theory in Isabelle/HOL, A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq, Formalising Semantics for Expected Running Time of Probabilistic Programs, Towards the Formal Reliability Analysis of Oil and Gas Pipelines, 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, Probabilistic guarded commands mechanized in HOL, Formal security proofs with minimal fuss: implicit computational complexity at work, On the formalization of gamma function in HOL, Generating functions for probabilistic programs