J. H. Anderson and Y. Kim, Adaptive Mutual Exclusion with Local Spinning, Proc. of ISDC'00, pp.29-43, 1914.
DOI : 10.1007/3-540-40026-5_2

J. H. Anderson, Y. Kim, and T. Herman, Shared-memory mutual exclusion: major research trends since 1986, Distributed Computing, vol.16, issue.2-3, pp.75-110, 2003.
DOI : 10.1007/s00446-003-0088-6

Y. Bar-david and G. Taubenfeld, Automatic discovery of mutual exclusion algorithms, Proc. of DISC'03, pp.136-150, 2003.

M. Botincan, AsmL specification and verification of Lamport's bakery algorithm, 27th International Conference on Information Technology Interfaces, 2005., pp.313-319, 2005.
DOI : 10.1109/ITI.2005.1491194

J. E. Burns and N. A. Lynch, Mutual exclusion using indivisible reads and writes, Proc. of ACCCC'80, pp.833-842, 1980.

D. Champelovier, X. Clerc, H. Garavel, Y. Guerte, F. Lang et al., Reference manual of the LOTOS NT to LOTOS translator (Version 5.0) INRIA/VASY, 2010.

G. Chehaibar, M. Zidouni, and R. Mateescu, Modeling Multiprocessor Cache Protocol Impact on MPI Performance, 2009 International Conference on Advanced Information Networking and Applications Workshops, 2009.
DOI : 10.1109/WAINA.2009.117
URL : https://hal.archives-ouvertes.fr/inria-00381674

T. S. Craig, Building FIFO and priority-queuing spin locks from atomic swap, 1993.

G. Delzanno and A. Podelski, Model Checking in CLP, Proc. of TACAS'99, pp.223-239, 1999.
DOI : 10.1007/3-540-49059-0_16

E. W. Dijkstra, Solution of a problem in concurrent programming control, Communications of the ACM, vol.8, issue.9, pp.569-570, 1965.
DOI : 10.1145/365559.365617

E. W. Dijkstra, Co-operating sequential processes, pp.43-112, 1968.

E. A. Emerson and C. Lei, Efficient model checking in fragments of the propositional mu-calculus, Proc. of LICS'86, pp.267-278, 1986.

M. J. Fischer and R. E. Ladner, Propositional dynamic logic of regular programs, Journal of Computer and System Sciences, vol.18, issue.2, pp.194-211, 1979.
DOI : 10.1016/0022-0000(79)90046-1

H. Garavel, OPEN/C??SAR: An open software architecture for verification, simulation, and testing, Proc. of TACAS'98, pp.68-84, 1998.
DOI : 10.1007/BFb0054165

H. Garavel and H. Hermanns, On Combining Functional Verification and Performance Evaluation Using CADP, Proc. of FME'02, pp.410-429, 2002.
DOI : 10.1007/3-540-45614-7_23
URL : https://hal.archives-ouvertes.fr/inria-00072096

H. Garavel and F. Lang, SVL: A Scripting Language for Compositional Verification, Proc. of FORTE'01, pp.377-392, 2001.
DOI : 10.1007/0-306-47003-9_24
URL : https://hal.archives-ouvertes.fr/inria-00072396

H. Garavel, F. Lang, R. Mateescu, and W. Serwe, CADP??2006: A Toolbox for the Construction and Analysis of Distributed Processes, Proc. of CAV'07, pp.158-163, 2007.
DOI : 10.1007/978-3-540-73368-3_18
URL : https://hal.archives-ouvertes.fr/inria-00189021

H. Garavel and M. Sighireanu, Towards a second generation of FDTs ? rationale for the design of E-LOTOS, Proc. of FMICS'98, pp.187-230, 1998.

H. Hermanns, Interactive Markov chains and the quest for quantified quality, LNCS 2428, 2002.

H. Hermanns and C. Joubert, A Set of Performance and Dependability Analysis Components for CADP, Proc. of TACAS'03, pp.425-430, 2003.
DOI : 10.1007/3-540-36577-X_30

H. Hermanns and J. Katoen, Performance Evaluation:= (Process Algebra + Model Checking) X Markov Chains, Proc. of CONCUR'01, pp.59-81, 2001.
DOI : 10.1007/3-540-44685-0_6
URL : http://eprints.eemcs.utwente.nl/6448/01/85_HermannsKatoen.pdf

H. Hermanns and M. Siegle, Bisimulation Algorithms for Stochastic Process Algebras and Their BDD-Based Implementation, Proc. of ARTS'99, pp.244-265, 1999.
DOI : 10.1007/3-540-48778-6_15
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.34.9799

I. Iec, Enhancements to LOTOS (E-LOTOS) International Standard 15437, International Organization for Standardization, 2001.

H. E. Jensen and N. A. Lynch, A proof of burns N-process mutual exclusion algorithm using abstraction, Proc. of TACAS'98, pp.409-423, 1998.
DOI : 10.1007/BFb0054186

J. L. Kessels, Arbitration without common modifiable variables, Acta Informatica, vol.12, issue.4, pp.135-141, 1982.
DOI : 10.1007/BF00288966

D. E. Knuth, Additional comments on a problem in concurrent programming control, Communications of the ACM, vol.9, issue.5, pp.321-322, 1966.
DOI : 10.1145/355592.365595

L. Lamport, A fast mutual exclusion algorithm, ACM Transactions on Computer Systems, vol.5, issue.1, pp.1-11, 1987.
DOI : 10.1145/7351.7352

P. S. Magnusson, A. Landin, and E. Hagersten, Queue locks on cache coherent multiprocessors, Proceedings of 8th International Parallel Processing Symposium, pp.165-171, 1994.
DOI : 10.1109/IPPS.1994.288305

Z. Manna and A. Pnueli, Tools and rules for the practicing verifier, pp.125-159, 1991.

Z. Manna and A. Pnueli, The temporal logic of reactive and concurrent systems, volume I (specification), 1992.

R. Mateescu, CAESAR_SOLVE: A generic library for on-the-fly resolution of alternation-free Boolean equation systems, International Journal on Software Tools for Technology Transfer, vol.8, issue.1, pp.37-56, 2006.
DOI : 10.1007/s10009-005-0194-9
URL : https://hal.archives-ouvertes.fr/inria-00084628

R. Mateescu and D. Thivolle, A model checking language for concurrent valuepassing systems, Proc. of FM'08, pp.148-164, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00315312

J. M. Mellor-crummey and M. L. Scott, Algorithms for scalable synchronization on shared-memory multiprocessors, ACM Transactions on Computer Systems, vol.9, issue.1, pp.21-65, 1991.
DOI : 10.1145/103727.103729
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.106.3994

R. D. Nicola and F. W. Vaandrager, Action versus state based logics for transition systems, LNCS, vol.469, pp.407-419, 1990.
DOI : 10.1007/3-540-53479-2_17

G. L. Peterson, Myths about the mutual exclusion problem, Information Processing Letters, vol.12, issue.3, pp.115-116, 1981.
DOI : 10.1016/0020-0190(81)90106-X

M. L. Puterman, Markov decision processes: discrete stochastic dynamic programming, 1994.
DOI : 10.1002/9780470316887

R. Streett, Propositional Dynamic Logic of looping and converse, Proceedings of the thirteenth annual ACM symposium on Theory of computing , STOC '81, pp.121-141, 1982.
DOI : 10.1145/800076.802492

B. K. Szymanski, A simple solution to Lamport's concurrent programming problem with linear wait, Proceedings of the 2nd international conference on Supercomputing , ICS '88, pp.621-626, 1988.
DOI : 10.1145/55364.55425

G. Taubenfeld, The Black-White Bakery Algorithm and Related Bounded-Space, Adaptive, Local-Spinning and FIFO Algorithms, Proc. of DISC'04, pp.56-70, 2004.
DOI : 10.1007/978-3-540-30186-8_5

G. Taubenfeld, Synchronization algorithms and concurrent programming, 2006.

J. Yang and J. H. Anderson, A fast, scalable mutual exclusion algorithm, Distributed Computing, vol.9, issue.1, pp.51-60, 1995.
DOI : 10.1007/BF01784242
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.34.8678

L. Zhang and M. R. Neuhäußer, Model Checking Interactive Markov Chains, Proc. of TACAS'10, pp.53-68, 2010.
DOI : 10.1007/978-3-642-12002-2_5

X. Zhang, Y. Yan, and R. Castaneda, Evaluating and designing software mutual exclusion algorithms on shared-memory multiprocessors, IEEE Parallel & Distributed Technology: Systems & Applications, vol.4, issue.1, pp.25-42, 1996.
DOI : 10.1109/88.481663