Abstract
We introduce a formal framework for reasoning about performance-style properties of probabilistic programs at the level of program code. Drawing heavily on the refinement-style of program verification, our approach promotes abstraction and proof re-use. The theory and proof tools to facilitate the verification have been implemented in HOL.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Celiku, O., McIver, A.: Cost-based analysis of probabilistic programs mechanised in HOL. Nordic Journal of Computing 11(2), 102–128 (2004)
Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)
Erlangen-Twente Markov Chain Checker, http://www.informatik.uni-erlangen.de/etmcc/
Fidge, C.J., Shankland, C.: But what if I don’t want to wait forever? Formal Aspects of Computing 15(2-3), 258–279 (2003)
Gordon, M.J.C., Melham, T.F.: Introduction to HOL A theorem-proving environment for higher order logic. Cambridge University Press, Cambridge (1993)
Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press, Cambridge (1996)
Hurd, J.: Formal Verification of Probabilistic Algorithms. PhD thesis, University of Cambridge (2002)
Hurd, J., McIver, A., Morgan, C.: Probabilistic guarded commands mechanized in HOL. In: Proc. of QAPL 2004 (March 2004)
Institute of Electrical and Electronics Engineers. IEEE Standard for a High Performance Serial Bus (Ammendment). Std 1394a-2000 (June 2000)
Knuth, D.E., Yao, A.C.: The complexity of nonuniform random number generation. In: Traub, J.F. (ed.) Algorithms and Complexity: New Directions and Recent Results. Academic Press, London (1976)
Kozen, D.: A probabilistic PDL. In: Proceedings of the 15th ACM Symposium on Theory of Computing (1983)
Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic symbolic model checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol. 2324, pp. 200–204. Springer, Heidelberg (2002)
McIver, A., Morgan, C.: Abstraction, refinement and proof for probabilistic systems. Springer, Heidelberg (2004)
Morgan, C., McIver, A.: pGCL: Formal reasoning for random algorithms. South African Computer Journal 22, 14–27 (1999)
Morgan, C.C.: Programming from Specifications. Prentice-Hall, Englewood Cliffs (1990)
Nipkow, T.: Hoare logics in Isabelle/HOL. In: Schwichtenberg, H., Steinbrüggen, R. (eds.) Proof and System-Reliability, pp. 341–367. Kluwer, Dordrecht (2002)
Stoelinga, M.: Fun with FireWire: A comparative study of formal verification methods applied to the IEEE 1394 root contention protocol. Formal Aspects of Computing 4(3), 328–337 (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Celiku, O., McIver, A. (2005). Compositional Specification and Analysis of Cost-Based Properties in Probabilistic Programs. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds) FM 2005: Formal Methods. FM 2005. Lecture Notes in Computer Science, vol 3582. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11526841_9
Download citation
DOI: https://doi.org/10.1007/11526841_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27882-5
Online ISBN: 978-3-540-31714-2
eBook Packages: Computer ScienceComputer Science (R0)