R. Back and W. Joakim-von, Duality in specification languages: a lattice-theoretical approach, Acta Informatica, vol.27, issue.7, pp.583-625, 1990.

A. Banerjee, D. A. Naumann, and M. Nikouei, Relational Logic with Framing and Hypotheses, Foundations of Software Technology and Theoretical Computer Science (Leibniz International Proceedings in Informatics), vol.65, p.16, 2016.

G. Barthe, J. M. Crespo, and C. Kunz, Relational Verification Using Product Programs, International Conference on Formal Methods, vol.6664, pp.200-214, 2011.

R. Bornat, Proving Pointer Programs in Hoare Logic, Mathematics of Program Construction, pp.102-126, 2000.

M. Clochard, Hoare Logic and Games, 2018.

M. Clochard, Méthodes et outils pour la spécification et la preuve de propriétés difficiles de programmes séquentiels, 2018.

M. Clochard, J. Filliâtre, and C. Marché, Variations on the McCarthy's 91 Function, 2018.

M. Clochard and C. Marché, Schorr-Waite Algorithm proved using a Ghost Monitor, 2018.

M. Clochard, A. Paskevich, and C. Marché, Deductive Verification via Ghost Debugging, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01907894

W. Edsger and . Dijkstra, Guarded commands, nondeterminacy and formal derivation of programs, Commun. ACM, vol.18, pp.453-457, 1975.

J. Filliâtre, L. Gondelman, and A. Paskevich, The Spirit of Ghost Code, Formal Methods in System Design, vol.48, pp.152-174, 2016.

M. Kiefer, V. Klebanov, and M. Ulbrich, Relational Program Reasoning Using Compiler IR, Journal of Automated Reasoning, vol.60, pp.337-363, 2018.

R. Krebbers, R. Jung, A. Bizjak, J. Jourdan, D. Dreyer et al., The Essence of Higher-Order Concurrent Separation Logic, 26th European Symposium on Programming Languages and Systems, vol.10201, pp.696-723, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01633133

K. Rustan and M. Leino, Dafny: An Automatic Program Verifier for Functional Correctness, LPAR-16, vol.6355, pp.348-370, 2010.

K. Mamouras, Synthesis of Strategies Using the Hoare Logic of Angelic and Demonic Nondeterminism, Logical Methods in Computer Science, vol.12, p.3, 2016.

Z. Manna and J. Mccarthy, Properties of programs and partial function logic, vol.5, pp.79-98, 1970.

G. Mével, J. Jourdan, and F. Pottier, Time Credits and Time Receipts in Iris, European Symposium on Programming (LNCS), Luís Caires, vol.11423, pp.3-29, 2019.

M. O. Myreen, J. C. Michael, and . Gordon, Hoare Logic for Realistically Modelled Machine Code, Tools and Algorithms for the Construction and Analysis of Systems, pp.568-582, 2007.

H. Schorr and W. M. Waite, An efficient machine-independent procedure for garbage collection in various list structures, Commun. ACM, vol.10, pp.501-506, 1967.

J. Tassarotti, R. Jung, and R. Harper, A Higher-Order Logic for Concurrent Termination-Preserving Refinement, European Symposium on Programming (Lecture Notes in Computer Science), Hongseok Yang, vol.10201, pp.909-936, 2017.

T. Tuerk, Local Reasoning about While-Loops. VS-Theory Workshop, 3rd Int. Conf. on Verified Software: Theories, Tools and Experiments, 2010.

M. Ulbrich, Dynamic Logic for an Intermediate Language Verification, Interaction and Refinement, Ph.D. Dissertation. Karlsruhe Institute of Technology, pp.90-411691, 2013.

H. Yang, Relational Separation Logic, Theoretical Computer Science, vol.375, pp.308-334, 2007.