scientific article; zbMATH DE number 2147036

MaRDI QIDQ4658722zbMATH OpenFDO

Authors Orieta Celiku, Annabelle McIver

Publication date 18 March 2005

zbMATH Keywords

expected time boundsHOLnondeterminismprobabilityprogram refinementquantitative program logic

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• FM 2005: Formal Methods
• Formalising Semantics for Expected Running Time of Probabilistic Programs
• Probabilistic analysis of programs: a weak limit approach
• Weakest precondition reasoning for expected run-times of probabilistic programs
• Quantitative program logic and expected time bounds in probabilistic distributed algorithms.

Cited in

(10)

• An elementary proof that Herman's ring is \(\Theta (N^{2})\)
• Axiomatic-like performance analysis (ALPA)
• Quantitative program logic and expected time bounds in probabilistic distributed algorithms.
• Markov chains and Markov decision processes in Isabelle/HOL
• Probabilistic guarded commands mechanized in HOL
• Probabilistic guarded commands mechanized in HOL
• Probabilistic analysis of programs: a weak limit approach
• Automating program analysis
• FM 2005: Formal Methods
• Type-based complexity analysis of probabilistic functional 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 Q4658722)