B. Alpern and F. B. Schneider, Recognizing safety and liveness, Distributed Computing, vol.56, issue.1???2, pp.117-126, 1987.
DOI : 10.1007/BF01782772
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.20.5470

B. Alpern and F. Schneider, Verifying temporal properties without temporal logic, ACM Transactions on Programming Languages and Systems, vol.11, issue.1, pp.147-167, 1989.
DOI : 10.1145/59287.62028
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.20.5721

D. Aspinall, S. Gilmore, M. Hofmann, D. Sannella, and I. Stark, Mobile Resource Guarantees for Smart Devices, Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, International Workshop (CASSIS'04) Barthe, L. Burdy, M. Huisman, J.-L, 2005.
DOI : 10.1007/978-3-540-30569-9_1

L. Bauer, J. Ligatti, and D. Walker, Composing security policies with Polymer, ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'05), pp.305-314, 2005.
DOI : 10.1145/1065010.1065047
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.70.498

N. Bielova, N. Dragoni, F. Massacci, K. Naliuka, and I. Siahaan, Matching in security-by-contract for mobile code, The Journal of Logic and Algebraic Programming, vol.78, issue.5, pp.340-358, 2009.
DOI : 10.1016/j.jlap.2009.02.013

N. Bielova and F. Massacci, Do You Really Mean What You Actually Enforced?, Lecture Notes in Computer Science, vol.5491, pp.287-301, 2008.
DOI : 10.1007/978-3-642-01465-9_19
URL : http://eprints.biblio.unitn.it/1449/1/techRep033.pdf

A. Brown, R. , and M. , Synthesising Monitors from High-Level Policies for the Safe Execution of Untrusted Software, 4th International Conference on Information Security Practice and Experience (ISPEC'08), pp.233-247, 2008.
DOI : 10.1007/978-3-540-79104-1_17

T. Colcombet and P. Fradet, Enforcing trace properties by program transformation, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '00, pp.54-66
DOI : 10.1145/325694.325703
URL : https://hal.archives-ouvertes.fr/inria-00000937

W. Enck, P. Gilbert, B. Chun, L. P. Cox, J. Jung et al., TaintDroid, 9th USENIX Symposium on Operating Systems Design and Implementation (OSDI'10) USENIX Association. 10. Erlingsson, ´ U., and Schneider, F. B. IRM enforcement of Java stack inspection IEEE Symposium on Security and Privacy (S&P'00), pp.246-255, 2000.
DOI : 10.1145/2619091

P. W. Fong, Access control by tracking shallow execution history, IEEE Symposium on Security and Privacy, 2004. Proceedings. 2004, pp.43-55, 2004.
DOI : 10.1109/SECPRI.2004.1301314
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.129.1172

D. Gurov, M. Huisman, and C. Sprenger, Compositional verification of sequential programs with procedures, Information and Computation, vol.206, issue.7, pp.840-868, 2008.
DOI : 10.1016/j.ic.2008.03.003

M. Huisman and A. Tamalet, A Formal Connection between Security Automata and JML Annotations, 12th International Conference on Fundamental Approaches to Software Engineering (FASE'09), pp.340-354, 2009.
DOI : 10.1007/978-3-642-00593-0_23

T. P. Jensen, L. Métayer, D. Thorn, and T. , Verification of control flow based security properties, Proceedings of the 1999 IEEE Symposium on Security and Privacy (Cat. No.99CB36344), pp.89-103, 1999.
DOI : 10.1109/SECPRI.1999.766902

G. Klein and T. Nipkow, Verified lightweight bytecode verification, Concurrency and Computation: Practice and Experience, vol.1690, issue.13, pp.1133-1151, 2001.
DOI : 10.1002/cpe.597
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.152.7227

J. Ligatti, L. Bauer, and D. Walker, Edit automata: enforcement mechanisms for run-time security policies, International Journal of Information Security, vol.3, issue.1-2, pp.1-2, 2005.
DOI : 10.1007/s10207-004-0046-8
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.114.6074

J. Ligatti, L. Bauer, and D. Walker, Enforcing Non-safety Security Policies with Program Monitors, 10th European Symposium on Research in Computer Security (ESORICS'05), pp.355-373, 2005.
DOI : 10.1007/11555827_21
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.118.7862

F. Massacci and I. Siahaan, Simulating midlet's security claims with automata modulo theory In Workshop on Programming Languages and Analysis for Security (PLAS'08), pp.1-9, 2008.

M. Mizuno and D. A. Schmidt, A security flow control algorithm and its denotational semantics correctness proof, Formal Aspects of Computing, vol.69, issue.2, pp.6-727, 1992.
DOI : 10.1007/BF03180570

G. Morrisett, D. Walker, K. Crary, and N. Glew, From system F to typed assembly language, ACM Transactions on Programming Languages and Systems, vol.21, issue.3, pp.527-568, 1999.
DOI : 10.1145/319301.319345

A. C. Myers, JFlow, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '99, pp.228-241, 1999.
DOI : 10.1145/292540.292561

G. C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '97, pp.106-119, 1997.
DOI : 10.1145/263699.263712

M. Ongtang, S. E. Mclaughlin, W. Enck, and P. Mcdaniel, Semantically rich applicationcentric security in Android, 25th Annual Computer Security Applications Conference (ACSAC'09), pp.340-349, 2009.

F. Pottier, C. Skalka, and S. F. Smith, A systematic approach to static access control, ACM Transactions on Programming Languages and Systems, vol.27, issue.2, pp.344-382, 2005.
DOI : 10.1145/1057387.1057392

E. Rose, Lightweight Bytecode Verification, Journal of Automated Reasoning, vol.31, issue.3/4, pp.3-4, 2003.
DOI : 10.1023/B:JARS.0000021015.15794.82
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.106.647

F. B. Schneider, Enforceable security policies, ACM Transactions on Information and System Security, vol.3, issue.1, pp.30-50, 2000.
DOI : 10.1145/353323.353382
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.147.1853

R. Sekar, V. N. Venkatakrishnan, S. Basu, S. Bhatkar, and D. C. Duvarney, Model-carrying code: a practical approach for safe execution of untrusted applications, 19th ACM Symposium on Operating Systems Principles (SOSP'03), pp.15-28, 2003.

C. Talhi, N. Tawbi, and M. Debbabi, Execution monitoring enforcement for limited-memory systems, Proceedings of the 2006 International Conference on Privacy, Security and Trust Bridge the Gap Between PST Technologies and Business Services, PST '06, pp.1-3812, 2006.
DOI : 10.1145/1501434.1501480

D. Vanoverberghe and F. Piessens, Supporting Security Monitor-Aware Development, Third International Workshop on Software Engineering for Secure Systems (SESS'07: ICSE Workshops 2007), pp.2-6, 2007.
DOI : 10.1109/SESS.2007.8
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.520.4098

D. Walker, A type system for expressive security policies, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '00, pp.254-267
DOI : 10.1145/325694.325728

S. Winwood, G. Klein, and M. M. Chakravarty, On the Automated Synthesis of Proof-Carrying Temporal Reference Monitors, 16th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'06), pp.111-126, 2006.
DOI : 10.1007/978-3-540-71410-1_9