A Graph-Based Implementation for Mechanized Refinement Calculus of OO Programs - Formal Methods: Foundations and Applications - page 273

5. Chen, Z., Liu, Z., Ravn, A.P., Stolz, V., Zhan, N.: Refinement and verification in
component-based model driven design. Science of Computer Programming 74(4),
168-196 (2009); UNU-IIST TR 388
6. Chen, Z., Liu, Z., Stolz, V.: The rCOS tool. In: Modelling and Analysis in VDM:
Proceedings of the Fourth VDM/Overture Workshop, number CS-TR-1099 in
Technical Report Series. Newcastle University (May 2008)
7. Chen, Z., Morisset, C., Stolz, V.: Specification and validation of behavioural pro-
tocols in the rCOS modeler. In: Arbab, F., Sirjani, M. (eds.) FSEN 2009. LNCS,
vol. 5961, pp. 387-401. Springer, Heidelberg (2010)
8. Depasse, C.: Constructing Isabelle proofs in a proof refinement calculus. Research
Report, UCL (2001)
9. Filliatre, J.-C.: Why: a multi-language multi-prover verification tool. Research Re-
port 1366, LRI, Universite Paris Sud (2003)
10. He, J., Liu, Z., Li, X.: rCOS: A refinement calculus of object systems. Theor.
Comput. Sci. 365(1-2), 109-142 (2006); UNU-IIST TR 322
11. Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice-Hall,

Englewood Cliffs (1998)
12. Ke, W., Liu, Z., Wang, S., Zhao, L.: A graph-based operational semantics of oo
programs. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885,
pp. 347-366. Springer, Heidelberg (2009)
13. Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual
machine, and compiler. ACM Trans. Program. Lang. Syst. 28(4), 619-695 (2006)
14. Laibinis, L.: Mechanised Formal Reasoning About Modular Programs. PhD thesis,
Abo Akademi (2000)
15. Lei, B., Liu, Z., Morisset, C., Li, X.: State based robustness testing for components.
In: FACS 2008. ENTCS, vol. 260, pp. 173-188. Elsevier, Amsterdam (2008)
16. Liu, Z., Morisset, C., Stolz, V.: rCOS: theory and tools for component-based model
driven development. In: Arbab, F., Sirjani, M. (eds.) FSEN 2009. LNCS, vol. 5961,
pp. 62-80. Springer, Heidelberg (2010)
17. Morgan, C.: Programming from specifications, 2nd edn. Prentice Hall International,
Englewood Cliffs (1994)
18. Paige, R., Ostroff, J., Brooke, P.: Formalising eiffel references and expanded types
in pvs. In: Proc. International Workshop on Aliasing, Confinement, and Ownership
in Object-Oriented Programming (2003)
19. Paige, R.F., Ostroff, J.S.: ERC - An object-oriented refinement calculus for Eiffel.
Form. Asp. Comput. 16(1), 51-79 (2004)
20. Sekerinski, E.: A type-theoretic basis for an object-oriented refinement calculus.
In: Formal Methods and Object Technology. Springer, Heidelberg (1996)
21. Stolz, V.: An integrated multi-view model evolution framework. Innovations in
Systems and Software Engineering (2009)
22. Utting, M.: An object-oriented refinement calculus with modular reasoning (1992)
23. van den Berg, J., Jacobs, B.: The loop compiler for java and jml. In: Margaria, T.,
Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 299-312. Springer, Heidelberg
(2001)
24. von Wright, J.: Program refinement by theorem prover. In: BCS FACS Sixth Refine-
ment Workshop - Theory and Practise of Formal Software Development. Springer,
Heidelberg (1994)