Automated Quantitative Software Verification.
Ph.D. thesis, Oxford University.
[Thesis on quantitative verification for software, including probabilistic abstraction-refinement methods that use components from GOTO-CC, SATABS and PRISM.]
Mark Kattenbelt, Marta Kwiatkowska, Gethin Norman and David Parker.
Abstraction Refinement for Probabilistic Software.
In Proc. 10th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'09), volume 5403 of Lecture Notes in Computer Science, pages 182-197, Springer.
[Develops verification techniques for probabilistic C programs, using components from GOTO-CC, SATABS and PRISM.]