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

R. Krzysztof and . Apt, Ten years of Hoare's logic: A survey?part I, ACM Trans. Program. Lang. Syst, vol.3, issue.4, pp.431-483, 1981.

C. Benzmüller and B. W. Paleo, Gödel's God on the computer, 10th Intl. Workshop Implementation of Logics, EPiC Series. EasyChair, 2013.

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.
DOI : 10.1007/978-94-011-5292-1

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
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.2.4409

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

O. Hans-jürgen, Semantics-based translation methods for modal logics, J. Log. Comput, vol.1, issue.5, pp.691-746, 1991.