M. Abadi and L. Lamport, The existence of refinement mappings, Theoretical Comput. Sci, vol.81, issue.2, pp.253-284, 1991.

K. R. Apt, Ten Years of Hoare's Logic: A Survey---Part I, ACM Transactions on Programming Languages and Systems, vol.3, issue.4, pp.431-483, 1981.
DOI : 10.1145/357146.357150

C. Benzmüller and B. Paleo, Automating Gödel's ontological proof of God's existence with higher-order automated theorem provers, 21st Europ. Conf. Artificial Intelligence, pp.93-98, 2014.

T. Braüner and S. Ghilardi, 9 First-order modal logic, Handbook of Modal Logic, pp.549-620, 2007.
DOI : 10.1016/S1570-2464(07)80012-7

D. Cousineau, D. Doligez, L. Lamport, S. Merz, D. Ricketts et al., TLA???+??? Proofs, 18th Intl. Symp. Formal Methods, pp.147-154, 2012.
DOI : 10.1007/978-3-642-32759-9_14

URL : https://hal.archives-ouvertes.fr/hal-00726632

M. Fitting and R. L. Mendelsohn, First-Order Modal Logic. Synthese Library, 1998.

H. Ganzinger, R. Nieuwenhuis, and P. Nivela, The Saturate system, 1998.

F. Giunchiglia and R. Sebastiani, Building Decision Procedures for Modal Logics from Propositional Decision Procedures: The Case Study of Modal K(m), Information and Computation, vol.162, issue.1-2, pp.158-178, 2000.
DOI : 10.1006/inco.1999.2850

U. Hustadt and R. A. Schmidt, MSPASS: Modal Reasoning by Translation and First-Order Resolution, LNCS, vol.1847, pp.67-71, 2000.
DOI : 10.1007/10722086_7

L. Lamport, Specifying Systems, The TLA + Language and Tools for Hardware and Software Engineers, 2002.

L. Lamport, Byzantizing Paxos by Refinement, Distributed Computing: 25th Intl. Symp. (DISC 2011), pp.211-224, 2011.
DOI : 10.1007/978-3-642-03466-4_2

H. J. Ohlbach, Semantics-Based Translation Methods for Modal Logics, Journal of Logic and Computation, vol.1, issue.5, pp.691-746, 1991.
DOI : 10.1093/logcom/1.5.691