M. Balliu, Logics for information flow security: from specification to verification, 2014.

G. Smith, Principles of Secure Information Flow Analysis, pp.291-307, 2007.
DOI : 10.1007/978-0-387-44599-1_13

A. Sabelfeld and A. C. Myers, Language-based information-flow security, IEEE Journal on Selected Areas in Communications, vol.21, issue.1, pp.5-19, 2003.
DOI : 10.1109/JSAC.2002.806121

D. Denning, A lattice model of secure information flow, Communications of the ACM, vol.19, issue.5, pp.236-243, 1976.
DOI : 10.1145/360051.360056

S. Zdancewic and A. C. Myers, Observational determinism for concurrent program security, 16th IEEE Computer Security Foundations Workshop, 2003. Proceedings., p.16, 2003.
DOI : 10.1109/CSFW.2003.1212703

J. Mclean, Proving Noninterference and Functional Correctness Using Traces, Journal of Computer Security, vol.1, issue.1, pp.37-57, 1992.
DOI : 10.3233/JCS-1992-1103

A. W. Roscoe, CSP and determinism in security modelling, Proceedings 1995 IEEE Symposium on Security and Privacy, 1995.
DOI : 10.1109/SECPRI.1995.398927

M. Huisman, P. Worah, and K. Sunesen, A temporal logic characterisation of observational de-terminism, Computer Security Foundations Workshop, p.19, 2006.

M. R. Clarkson, B. Finkbeiner, M. Koleini, K. K. Micinski, M. N. Rabe et al., Temporal Logics for Hyperproperties, Principles of Security and Trust, pp.265-284, 2014.
DOI : 10.1007/978-3-642-54792-8_15

C. Baier and J. P. Katoen, Principles of model checking, 2008.

T. Terauchi, A Type System for Observational Determinism, 2008 21st IEEE Computer Security Foundations Symposium, pp.287-300, 2008.
DOI : 10.1109/CSF.2008.9

J. F. Groote and F. Vaandrager, An efficient algorithm for branching bisimulation and stutter-ing equivalence, pp.626-638, 1990.

A. Chutinan and B. H. Krogh, Verification of infinite-state dynamic systems using approximate quotient transition systems, IEEE Transactions on Automatic Control, vol.46, issue.9, pp.1401-1410, 2001.
DOI : 10.1109/9.948467

T. M. Ngo, Qualitative and quantitative information flow analysis for multi-thread pro-grams, 2014.

M. Huisman and H. C. Blondeel, Model-checking secure information flow for multithreaded programs, Theory of Security and Applications, pp.148-165, 2012.

T. M. Ngo, M. Stoelinga, and M. Huisman, Effective verification of confidentiality for multi-threaded programs, Journal of Computer Security, vol.22, issue.2, pp.269-300, 2014.
DOI : 10.3233/JCS-130492

D. Volpano, C. Irvine, and G. Smith, A sound type system for secure flow analysis, Jour-nal of computer security, pp.167-187, 1996.
DOI : 10.3233/JCS-1996-42-304

G. Smith and D. Volpano, Secure information flow in a multi-threaded imperative language, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '98, pp.355-364, 1998.
DOI : 10.1145/268946.268975

G. Barthe, P. R. Rezk, and T. , Secure information flow by self-composition

J. Mclean, A general theory of composition for trace sets closed under selective interleav-ing functions, Research in Security and Privacy, Proceedings, IEEE Computer Society Symposium on, pp.79-93, 1994.

M. R. Clarkson and F. B. Schneider, Hyperproperties, Journal of Computer Security, vol.18, issue.6, pp.1157-1210, 2010.
DOI : 10.3233/JCS-2009-0393

E. M. Clarke, The Birth of Model Checking, pp.1-26, 2008.
DOI : 10.1007/978-3-540-69850-0_1

E. A. Emerson, The beginning of model checking: A personal perspective In: 25 Years of Model Checking, pp.27-45, 2008.

B. Finkbeiner, M. N. Rabe, and C. Snchez, A temporal logic for hyperproperties. In: arXiv preprint arXiv:1306, p.6657, 2013.

R. Dimitrova, B. Finkbeiner, M. Kovcs, M. N. Rabe, and H. Seidl, Model checking infor-mation flow in reactive systems, Model Checking, and Abstract Interpreta-tion, pp.169-185, 2012.

H. Mantel, Unwinding Possibilistic Security Properties, pp.238-254, 2000.
DOI : 10.1007/10722599_15

D. Souza, D. Holla, R. Raghavendra, K. R. Sprick, and B. , Model-checking trace-based information flow properties*, Journal of Computer Security, vol.19, issue.1, pp.101-138, 2011.
DOI : 10.3233/JCS-2010-0400