M. Abadi, The Prophecy of Undo, Fundamental Approaches to Software Engineering, pp.347-361, 2015.
DOI : 10.1007/978-3-662-46675-9_23

M. Abadi and L. Lamport, The existence of refinement mappings, Theoretical Computer Science, vol.82, issue.2, pp.253-284, 1991.
DOI : 10.1016/0304-3975(91)90224-P

Y. Afek, H. Attiya, D. Dolev, E. Gafni, M. Merritt et al., Atomic snapshots of shared memory, Journal of the ACM, vol.40, issue.4, pp.873-890, 1993.
DOI : 10.1145/153724.153741
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.4013

M. P. Herlihy and J. M. Wing, Axioms for concurrent objects, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '87, pp.13-26, 1987.
DOI : 10.1145/41625.41627
URL : http://repository.cmu.edu/cgi/viewcontent.cgi?article=2597&context=compsci

C. A. Hoare, Proof of correctness of data representations, Acta Informatica, vol.12, issue.4, pp.271-281, 1972.
DOI : 10.1007/BF00289507

L. Lamport, Auxiliary variables in TLA+ Web page at URL http

L. Lamport, TLA?temporal logic of actions. A web page, a link to which can be found at URL http://lamport.org. The page can also be found by searching the Web for the 21-letter string formed by concatenating uid and lamporttlahomepage

L. Lamport, Specifying Systems A link to an electronic copy can be found at http, 2003.

S. Owicki and D. Gries, Verifying properties of parallel programs: an axiomatic approach, Communications of the ACM, vol.19, issue.5, pp.279-284, 1976.
DOI : 10.1145/360051.360224