C. Henry, J. Baker, and C. Hewitt, The incremental garbage collection of processes, Proceedings of the 1977 symposium on Artificial intelligence and programming languages, pp.55-59, 1977.

T. Ball and S. Rajamani, The SLAM Toolkit, CAV'01, pp.260-264, 2001.
DOI : 10.1007/3-540-44585-4_25

S. Bensalem, M. Bozga, T. H. Nguyen, and J. Sifakis, Compositional verification for component-based systems and application, ATVA'08, pp.181-193, 2010.
DOI : 10.1049/iet-sen.2009.0011

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

E. Clarke, D. Kroening, N. Sharygina, and K. Yorav, SATABS: SAT-Based Predicate Abstraction for ANSI-C, TACAS'05, pp.570-574, 2005.
DOI : 10.1007/978-3-540-31980-1_40

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

E. M. Clarke, O. Grumberg, and D. A. Peled, Model Checking, 1999.

M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-oliet et al., All about Maude -a high-performance logical framework: how to specify, program and verify systems in rewriting logic, LNCS, vol.4350, 2007.

R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi, Reasoning about knowledge, 1995.

A. Fehnker, R. J. Van-glabbeek, P. Höfner, A. Mciver, M. Portmann et al., Automated Analysis of AODV Using UPPAAL, TACAS'12, pp.173-187, 2012.
DOI : 10.1007/978-3-642-28756-5_13

G. J. Holzmann, The model checker SPIN, IEEE Transactions on Software Engineering, vol.23, issue.5, 2003.
DOI : 10.1109/32.588521

E. B. Johnsen, R. Hähnle, J. Schäfer, R. Schlatte, and M. Steffen, ABS: A Core Language for Abstract Behavioral Specification, FMCO'10, pp.142-164, 2011.
DOI : 10.2498/cit.2002.01.01

R. K. Karmani, A. Shali, and G. Agha, Actor frameworks for the JVM platform, Proceedings of the 7th International Conference on Principles and Practice of Programming in Java, PPPJ '09, pp.11-20, 2009.
DOI : 10.1145/1596655.1596658

W. Leister, J. Bjørk, R. Schlatte, and A. Griesmayer, Verifying distributed algorithms with executable Creol models, PESARO'11, pp.1-6, 2011.

C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, S. Bensalem et al., Property preserving abstractions for the verification of concurrent systems. Formal methods in system design, pp.11-44, 1995.

A. Lomuscio, W. Penczek, and H. Qu, Partial order reductions for model checking temporal epistemic logics over interleaved multi-agent systems, Fundamenta Informaticae, vol.101, issue.1, pp.71-90, 2010.
DOI : 10.1007/978-3-642-00431-5_7

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

A. Lomuscio, H. Qu, and F. Raimondi, MCMAS: A Model Checker for the Verification of Multi-Agent Systems, CAV'09, pp.682-688, 2009.
DOI : 10.1007/978-3-642-02658-4_55

A. Lomuscio, H. Qu, and M. Solanki, Towards verifying contract regulated service composition, Autonomous Agents and Multi-Agent Systems, vol.126, issue.2, pp.345-373, 2010.
DOI : 10.1007/s10458-010-9152-3

URL : http://spiral.imperial.ac.uk/bitstream/10044/1/13929/2/Autonomous%20Agents%20and%20Multi-Agent%20Systems_24_3_2012.pdf

M. Musuvathi, D. Y. Park, A. Chou, D. R. Engler, and D. L. Dill, CMC, ACM SIGOPS Operating Systems Review, vol.36, issue.SI, pp.75-88, 2002.
DOI : 10.1145/844128.844136

C. Perkins, E. Belding-royer, and S. Das, Ad hoc On-Demand Distance Vector (AODV) Routing, RFC, vol.3561, 2003.
DOI : 10.17487/rfc3561

G. Ramalingam, Context-sensitive synchronization-sensitive analysis is undecidable, ACM Transactions on Programming Languages and Systems, vol.22, issue.2, pp.416-430, 2000.
DOI : 10.1145/349214.349241

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

F. De-renesse and A. H. Aghvami, Formal verification of ad-hoc routing protocols using SPIN model checker, Proceedings of the 12th IEEE Mediterranean Electrotechnical Conference (IEEE Cat. No.04CH37521), pp.1177-1182, 2004.
DOI : 10.1109/MELCON.2004.1348275

V. Stolz and F. Huch, Runtime Verification of Concurrent Haskell Programs, RV'04, pp.201-216, 2005.
DOI : 10.1016/j.entcs.2004.01.026

W. Visser, K. Havelund, G. Brat, S. Park, and F. Lerda, Model checking programs, Proceedings ASE 2000. Fifteenth IEEE International Conference on Automated Software Engineering, pp.203-232, 2003.
DOI : 10.1109/ASE.2000.873645

T. Witkowski, N. Blanc, D. Kroening, and G. Weissenbacher, Model checking concurrent linux device drivers, Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering , ASE '07, pp.501-504, 2007.
DOI : 10.1145/1321631.1321719