Logics for information flow security: from specification to verification, 2014. ,
Principles of Secure Information Flow Analysis, pp.291-307, 2007. ,
DOI : 10.1007/978-0-387-44599-1_13
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
A lattice model of secure information flow, Communications of the ACM, vol.19, issue.5, pp.236-243, 1976. ,
DOI : 10.1145/360051.360056
Observational determinism for concurrent program security, 16th IEEE Computer Security Foundations Workshop, 2003. Proceedings., p.16, 2003. ,
DOI : 10.1109/CSFW.2003.1212703
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
CSP and determinism in security modelling, Proceedings 1995 IEEE Symposium on Security and Privacy, 1995. ,
DOI : 10.1109/SECPRI.1995.398927
A temporal logic characterisation of observational de-terminism, Computer Security Foundations Workshop, p.19, 2006. ,
Temporal Logics for Hyperproperties, Principles of Security and Trust, pp.265-284, 2014. ,
DOI : 10.1007/978-3-642-54792-8_15
Principles of model checking, 2008. ,
A Type System for Observational Determinism, 2008 21st IEEE Computer Security Foundations Symposium, pp.287-300, 2008. ,
DOI : 10.1109/CSF.2008.9
An efficient algorithm for branching bisimulation and stutter-ing equivalence, pp.626-638, 1990. ,
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
Qualitative and quantitative information flow analysis for multi-thread pro-grams, 2014. ,
Model-checking secure information flow for multithreaded programs, Theory of Security and Applications, pp.148-165, 2012. ,
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
A sound type system for secure flow analysis, Jour-nal of computer security, pp.167-187, 1996. ,
DOI : 10.3233/JCS-1996-42-304
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
Secure information flow by self-composition ,
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. ,
Hyperproperties, Journal of Computer Security, vol.18, issue.6, pp.1157-1210, 2010. ,
DOI : 10.3233/JCS-2009-0393
The Birth of Model Checking, pp.1-26, 2008. ,
DOI : 10.1007/978-3-540-69850-0_1
The beginning of model checking: A personal perspective In: 25 Years of Model Checking, pp.27-45, 2008. ,
A temporal logic for hyperproperties. In: arXiv preprint arXiv:1306, p.6657, 2013. ,
Model checking infor-mation flow in reactive systems, Model Checking, and Abstract Interpreta-tion, pp.169-185, 2012. ,
Unwinding Possibilistic Security Properties, pp.238-254, 2000. ,
DOI : 10.1007/10722599_15
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