, Proceedings of the 5th Annual Symp. on Logic in Computer Science (LICS '90), 1990.

M. Abadi, M. Budiu, Ú. Erlingsson, and J. Ligatti, Control-flow integrity principles, implementations, and applications, ACM Trans. Inf. Syst. Secur, vol.13, issue.1, 2009.

I. Aktug, M. Dam, and D. Gurov, Provably correct runtime monitoring, J. Log. Algebr. Program, vol.78, issue.5, pp.304-339, 2009.

B. Alpern and F. B. Schneider, Defining liveness, Inf. Process. Lett, vol.21, issue.4, pp.181-185, 1985.

R. Alur, C. Courcoubetis, and D. L. Dill, Model-checking for real-time systems, Proc. of the 5th Annual Symp. on Logic in Computer Science (LICS '90, pp.414-425

R. Alur and D. L. Dill, A theory of timed automata, Theoretical Computer Science, vol.126, pp.183-235, 1994.

R. Alur and T. A. Henzinger, Real-time logics: Complexity and expressiveness, Proc. of the Fifth Annual Symp. on Logic in Computer Science (LICS '90, pp.390-401

A. Amiar, M. Delahaye, Y. Falcone, L. Du-bousquet, G. Schirner et al., Compressing microcontroller execution traces to assist system analysis, Embedded Systems: Design, Analysis and Verification -4th IFIP TC 10 Int. Embedded Systems Symp., IESS 2013. IFIP Advances in Information and Communication Technology, vol.403, pp.139-150, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00853716

A. Amiar, M. Delahaye, Y. Falcone, and L. Du-bousquet, Fault localization in embedded software based on a single cyclic trace, IEEE 24th Int. Symp. on Software Reliability Engineering, pp.148-157, 2013.

A. A. De-amorim, C. Hritcu, and B. C. Pierce, The meaning of memory safety, Principles of Security and Trust -7th Int. Conf., POST 2018, Held as Part of the European Joint Conf.s on Theory and Practice of Software, ETAPS 2018, Proc. LNCS, vol.10804, pp.79-105, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01949201

R. Babaee, A. Gurfinkel, and S. Fischmeister, Predictive run-time verification of discrete-time reachability properties in black-box systems using trace-level abstraction and statistical learning, Colombo and Leucker, vol.30, pp.187-204

, Lectures on Runtime Verification -Introductory and Advanced Topics, vol.10457, 2018.

E. Bartocci, Y. Falcone, B. Bonakdarpour, C. Colombo, N. Decker et al., First int. competition on runtime verification: rules, benchmarks, tools, and final results of CRV, vol.21, pp.31-70, 2014.

E. Bartocci, Y. Falcone, A. Francalanza, and G. Reger, Introduction to runtime verification, Bartocci and Falcone, vol.12, pp.1-33
URL : https://hal.archives-ouvertes.fr/hal-01762297

A. Bauer and Y. Falcone, Decentralised LTL monitoring, Form. Meth. in Syst. Design, vol.48, issue.1-2, pp.46-93, 2016.
URL : https://hal.archives-ouvertes.fr/hal-00857286

D. Beauquier, J. Cohen, and R. Lanotte, Security policies enforcement using finite edit automata, Electr. Notes Theor. Comput. Sci, vol.229, issue.3, pp.19-35, 2009.

D. Beauquier, J. Cohen, and R. Lanotte, Security policies enforcement using finite and pushdown edit automata, Int. J. Inf. Sec, vol.12, issue.4, pp.319-336, 2013.

J. Bengtsson and W. Yi, Timed automata: Semantics, algorithms and tools, Proc. of the 4th Advanced Course on Petri Nets -Lecture Notes on Concurrency and Petri Nets, vol.3098, pp.87-124, 2003.

N. Bielova and F. Massacci, Do you really mean what you actually enforced?, Formal Aspects in Security and Trust, 5th Int. Workshop, FAST 2008, vol.5491, pp.287-301, 2008.

N. Bielova and F. Massacci, Predictability of enforcement, Engineering Secure Software and Systems -Third Int. Symp., ESSoS 2011s, vol.6542, pp.73-86, 2011.

N. Bielova and F. Massacci, Iterative enforcement by suppression: Towards practical enforcement theories, J. of Computer Security, vol.20, issue.1, pp.51-79, 2012.

A. Birgisson, M. Dhawan, Ú. Erlingsson, V. Ganapathy, and L. Iftode, Enforcing authorization policies using transactional memory introspection

, Proc. of the 2008 ACM Conf. on Computer and Communications Security, CCS, pp.223-234, 2008.

J. O. Blech, Y. Falcone, and K. Becker, Towards certified runtime verification, Formal Methods and Software Engineering -14th Int. Conference on Formal Engineering Methods, ICFEM 2012, vol.7635, pp.494-509, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00857287

D. Bruening and Q. Zhao, Practical memory checking with dr. memory, The 9th Int. Symp. on Code Generation and Optimization, pp.213-223, 2011.

D. Bruening and Q. Zhao, Using Dr. Fuzz, Dr. Memory, and custom dynamic tools for secure development, IEEE Cybersecurity Development, p.158, 2016.

H. Chabot, R. Khoury, and N. Tawbi, Extending the enforcement power of truncation monitors using static analysis, Computers & Security, vol.30, issue.4, pp.194-207, 2011.

E. Y. Chang, Z. Manna, and A. Pnueli, Characterization of temporal property classes, Automata, Languages and Programming, 19th Int. Colloquium, ICALP92. LNCS, vol.623, pp.474-486, 1992.

S. Chong, K. Vikram, and A. C. Myers, SIF: enforcing confidentiality and integrity in web applications, Proc. of the 16th USENIX Security Symp. USENIX Association, 2007.

C. Colombo and Y. Falcone, Organising LTL monitors over distributed systems with a global clock, Form. Meth. in Syst. Design, vol.49, issue.1-2, pp.109-158, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01120551

, Runtime Verification -18th Int. Conf., RV 2018, vol.11237, 2018.

C. Colombo and G. Pace, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools, An Int. Workshop on Competitions, vol.3, pp.55-63, 2017.

C. Colombo and G. J. Pace, Recovery within long-running transactions, ACM Comput. Surv, vol.45, issue.3, p.35, 2013.

M. Dam, B. Jacobs, A. Lundblad, and F. Piessens, Provably correct inline monitoring for multithreaded java-like programs, Journal of Computer Security, vol.18, issue.1, pp.37-59, 2010.

L. Davi, A. Sadeghi, and M. Winandy, ROPdefender: a detection tool to defend against returnoriented programming attacks, Proc. of the 6th ACM Symp. on Information, Computer and Communications Security, pp.40-51, 2011.

G. J. Duck, R. H. Yap, and L. Cavallaro, Stack bounds protection with low fat pointers, 24th Annual Network and Distributed System Security Symp, 2017.

K. El-harake, Y. Falcone, W. Jerad, M. Langet, and M. Mamlouk, Blocking advertisements on Android devices using monitoring techniques, Leveraging Applications of Formal Methods, Verification and Validation -6th Int. Symp, vol.8803, pp.239-253, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01120550

A. El-hokayem and Y. Falcone, THEMIS: a tool for decentralized monitoring algorithms, Proc. of the 26th ACM SIGSOFT Int. Symp. on Software Testing and Analysis, pp.372-375, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01653727

Ú. Erlingsson and F. B. Schneider, SASI enforcement of security policies: a retrospective, Proc. of the 1999 Workshop on New Security Paradigms, pp.87-95, 1999.

Y. Falcone, H. Barringer, Y. Falcone, B. Finkbeiner, K. Havelund et al., You should better enforce than verify, Runtime Verification -First Int. Conf., RV 2010, vol.6418, pp.89-105, 2010.
URL : https://hal.archives-ouvertes.fr/hal-00523653

Y. Falcone, T. Cornebize, and J. Fernandez, Efficient and generalized decentralized monitoring of regular languages, Formal Techniques for Distributed Objects, Components, and Systems -34th IFIP WG 6.1 Int. Conf., FORTE 2014, Held as Part of the 9th Int. Federated Conf. on Distributed Computing Techniques, vol.8461, pp.66-83, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00972559

Y. Falcone, S. Currea, and M. Jaber, Runtime verification and enforcement for Android applications with RV-Droid, Qadeer and Tasiran, vol.89, pp.88-95
URL : https://hal.archives-ouvertes.fr/hal-00857292

Y. Falcone, J. Fernandez, and L. Mounier, What can you verify and enforce at runtime? STTT, vol.14, pp.349-382, 2012.

Y. Falcone, K. Havelund, and G. Reger, A tutorial on runtime verification, Engineering Dependable Software Systems, NATO Science for Peace and Security Series, D: Information and Communication Security, vol.34, pp.141-175, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00853727

Y. Falcone, T. Jéron, H. Marchand, and S. Pinisetty, Runtime enforcement of regular timed properties by suppressing and delaying events, Sci. Comput. Program, vol.123, pp.2-41, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01281727

Y. Falcone, S. Krstic, G. Reger, and D. Traytel, A taxonomy for classifying runtime verification tools, Colombo and Leucker, vol.30, pp.241-262
URL : https://hal.archives-ouvertes.fr/hal-01882410

Y. Falcone and H. Marchand, Enforcement and validation (at runtime) of various notions of opacity, Discrete Event Dynamic Systems, vol.25, issue.4, pp.531-570, 2015.
URL : https://hal.archives-ouvertes.fr/hal-00987985

Y. Falcone, L. Mariani, A. Rollet, and S. Saha, Runtime failure prevention and reaction, Bartocci and Falcone, vol.12, pp.103-134
URL : https://hal.archives-ouvertes.fr/hal-01723606

Y. Falcone, L. Mounier, J. Fernandez, and J. Richier, Runtime enforcement monitors: composition, synthesis, and enforcement abilities, Form. Meth. in Syst. Design, vol.38, issue.3, pp.223-262, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00576948

A. Ferraiuolo, M. Zhao, A. C. Myers, and G. E. Suh, Hyperflow: A processor architecture for nonmalleable, timing-safe information flow security, Proc. of the 2018 ACM SIGSAC Conf. on Computer and Communications Security, CCS 2018, pp.1583-1600, 2018.

P. W. Fong, Access control by tracking shallow execution history, IEEE Symp. on Security and Privacy, pp.43-55, 2004.

A. Francalanza, J. A. Pérez, and C. Sánchez, Runtime verification for decentralised and distributed systems, Bartocci and Falcone, vol.12, pp.176-210

E. Göktas, E. Athanasopoulos, H. Bos, and G. Portokalidis, Out of control: Overcoming control-flow integrity, 2014 IEEE Symp, pp.575-589, 2014.

S. Hallé, R. Khoury, Q. Betti, A. El-hokayem, and Y. Falcone, Decentralized enforcement of document lifecycle constraints, Inf. Syst, vol.74, pp.117-135, 2018.

K. Havelund, G. Reger, D. Thoma, and E. Zalinescu, Monitoring events that carry data, Bartocci and Falcone, vol.12, pp.61-102

Y. Ji, Y. Wu, and S. Lafortune, Enforcement of opacity by public and private insertion functions, Automatica, vol.93, pp.369-378, 2018.

H. D. Johansen, E. Birrell, R. Van-renesse, F. B. Schneider, M. Stenhaug et al., Enforcing privacy policies with meta-code, Proc. of the 6th Asia-Pacific Workshop on Systems, vol.16, pp.1-16, 2015.

M. Kayaalp, M. Ozsoy, N. B. Abu-ghazaleh, and D. Ponomarev, Branch regulation: Lowoverhead protection from code reuse attacks, 39th Int. Symp. on Computer Architecture, pp.94-105, 2012.

R. Khoury and N. Tawbi, Corrective enforcement: A new paradigm of security policy enforcement by monitors, ACM Trans. Inf. Syst. Secur, vol.15, issue.2, p.27, 2012.

R. Khoury and N. Tawbi, Which security policies are enforceable by runtime monitors? A survey, Computer Science Review, vol.6, issue.1, pp.27-45, 2012.

G. Kiczales, Aspect-oriented programming, vol.96, p.730

G. Kiczales and M. Mezini, Aspect-oriented programming and modular reasoning, vol.96, pp.49-58

V. Kiriansky, D. Bruening, and S. P. Amarasinghe, Secure execution via program shepherding, Proc. of the 11th USENIX Security Symp, pp.191-206, 2002.

B. Könighofer, M. Alshiekh, R. Bloem, L. R. Humphrey, R. Könighofer et al., Shield synthesis, Form. Meth. in Syst. Design, vol.51, issue.2, pp.332-361, 2017.

E. Kozyri, O. Arden, A. C. Myers, F. B. Schneider, J. D. Guttman et al., JRIF: reactive information flow control for java, Foundations of Security, Protocols, and Equational Reasoning -Essays Dedicated to Catherine A. Meadows, vol.11565, pp.70-88, 2019.

A. Kumar, J. Ligatti, Y. Tu, J. Wang, W. Cellary et al., Query monitoring and analysis for database privacy -A security automata model approach, Web Information Systems Engineering -WISE 2015 -16th Int. Conf., Part II, vol.9419, pp.458-472, 2015.

L. Lamport, Proving the correctness of multiprocess programs, IEEE Trans. Software Eng, vol.3, issue.2, pp.125-143, 1977.

J. Lesage, J. Faure, and J. E. Cury, 12th Int. Workshop on Discrete Event Systems, WODES 2014. Int. Federation of Automatic Control, 2014.

J. Ligatti, L. Bauer, and D. Walker, Run-time enforcement of nonsafety policies, ACM Trans. Inf. Syst. Secur, vol.12, issue.3, p.41, 2009.

J. M. Lourenço, J. Fiedor, B. Krena, and T. Vojnar, Discovering concurrency errors, Bartocci and Falcone, vol.12, pp.34-60

Q. Luo and G. Rosu, Enforcemop: a runtime property enforcement system for multithreaded programs, Int. Symp. on Software Testing and Analysis, ISSTA. pp, pp.156-166, 2013.

Z. Manna and A. Pnueli, The temporal logic of reactive and concurrent systems -specification, 1992.

, Leveraging Applications of Formal Methods, Verification and Validation -7th Int. Symp, vol.9953, 2016.

F. Martinelli, I. Matteucci, P. Mori, and A. Saracino, Enforcement of U-XACML history-based usage control policy, Security and Trust Management -12th Int. Workshop, STM 2016, vol.9871, pp.64-81, 2016.

P. O. Meredith, D. Jin, D. Griffith, F. Chen, and G. Rosu, An overview of the MOP runtime verification framework, STTT, vol.14, issue.3, pp.249-289, 2012.

T. Nguyen, E. Bartocci, D. Nickovic, R. Grosu, S. Jaksic et al., The HARMONIA project: Hardware monitoring for automotive systems-of-systems, Margaria and Steffen, pp.371-379

J. A. Pavlich-mariscal, S. A. Demurjian, and L. D. Michel, A framework of composable access control definition, enforcement and assurance, XXVII Int. Conf. of the Chilean Computer Science Society, pp.13-22, 2008.

J. A. Pavlich-mariscal, S. A. Demurjian, and L. D. Michel, A framework for security assurance of access control enforcement code, Computers & Security, vol.29, issue.7, pp.770-784, 2010.

J. A. Pavlich-mariscal, L. Michel, and S. A. Demurjian, A formal enforcement framework for role-based access control using aspect-oriented programming, Model Driven Engineering Languages and Systems, 8th Int. Conf., MoDELS 2005, vol.3713, pp.537-552, 2005.

S. Pinisetty, Runtime enforcement of timed properties. (Enforcementà l'éxécution de propriétés temporisées), vol.1, 2015.
URL : https://hal.archives-ouvertes.fr/hal-00743270

S. Pinisetty, Y. Falcone, T. Jéron, and H. Marchand, Runtime enforcement of parametric timed properties with practical applications, vol.67, pp.420-427
URL : https://hal.archives-ouvertes.fr/hal-00974548

S. Pinisetty, Y. Falcone, T. Jéron, and H. Marchand, Runtime enforcement of regular timed properties, Symp. on Applied Computing, SAC 2014, pp.1279-1286, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00907571

S. Pinisetty, Y. Falcone, T. Jéron, and H. Marchand, Tipex: A tool chain for timed property enforcement during execution, Runtime Verification -6th Int. Conf., RV 2015, vol.9333, pp.306-320, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01244446

S. Pinisetty, Y. Falcone, T. Jéron, H. Marchand, A. Rollet et al., Runtime enforcement of timed properties revisited, Form. Meth. in Syst. Design, vol.45, issue.3, pp.381-422, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01088136

S. Pinisetty, Y. Falcone, T. Jéron, H. Marchand, A. Rollet et al., Runtime enforcement of timed properties, Qadeer and Tasiran, vol.89, pp.229-244
URL : https://hal.archives-ouvertes.fr/hal-00743270

S. Pinisetty, T. Jéron, S. Tripakis, Y. Falcone, H. Marchand et al., Predictive runtime verification of timed properties, J. of Systems and Software, vol.132, pp.353-365, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01666995

S. Pinisetty, V. Preoteasa, S. Tripakis, T. Jéron, Y. Falcone et al., Predictive runtime enforcement, Form. Meth. in Syst. Design, vol.51, issue.1, pp.154-199, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01647787

S. Pinisetty, P. S. Roop, S. Smyth, N. Allen, S. Tripakis et al., Runtime enforcement of cyber-physical systems, ACM Trans. Embed. Comput. Syst, vol.16, issue.5s, pp.1-178, 2017.

A. Pnueli, Embedded systems: Challenges in specification and verification, Embedded Software, Second International Conf, vol.2491, pp.1-14, 2002.

, Runtime Verification, Third Int. Conf., RV 2012, vol.7687, 2013.

G. Reger and K. Havelund, What is a trace? A runtime verification perspective, pp.339-355

M. Renard, Y. Falcone, A. Rollet, T. Jéron, and H. Marchand, Optimal enforcement of (timed) properties with uncontrollable events, Mathematical Structures in Computer Science, vol.29, issue.1, pp.169-214, 2019.
URL : https://hal.archives-ouvertes.fr/hal-01262444

M. Renard, Y. Falcone, A. Rollet, S. Pinisetty, T. Jéron et al., Enforcement of (timed) properties with uncontrollable events, Theoretical Aspects of Computing -ICTAC 2015 -12th Int. Colloquium. LNCS, vol.9399, pp.542-560, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01185238

M. Renard, A. Rollet, and Y. Falcone, Runtime enforcement using büchi games, Proc. of the 24th ACM SIGSOFT Int. SPIN Symp. on Model Checking of Software, pp.70-79, 2017.

O. Riganelli, D. Micucci, L. Mariani, and Y. Falcone, Verifying policy enforcers, Runtime Verification -17th Int. Conference, RV 2017, vol.10548, pp.241-258, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01653894

M. C. Rinard, R. Crocker, and G. Jr, Acceptability-oriented computing, Companion of the 18th Annual ACM SIGPLAN Conf. on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2003, pp.221-239, 2003.

G. Roman and W. G. Griswold, 27th Int. Conf. on Software Engineering (ICSE 2005), 2005.

S. Pinisetty, TiPEX website, 2015.

F. B. Schneider, Enforceable security policies, ACM Trans. Inf. Syst. Secur, vol.3, issue.1, pp.30-50, 2000.

K. Selyunin, T. Nguyen, E. Bartocci, D. Nickovic, and R. Grosu, Monitoring of MTL specifications with ibm's spiking-neuron model, 2016 Design, Automation & Test in Europe Conf. & Exhibition, DATE 2016, pp.924-929, 2016.

J. Seward and N. Nethercote, Using valgrind to detect undefined value errors with bit-precision, Proc. of the 2005 USENIX Annual Technical Conf, pp.17-30, 2005.

J. Sifakis, Modeling real-time systems, Proc. of the 25th IEEE Real-Time Systems Symp, pp.5-6, 2004.

J. Sifakis, S. Tripakis, and S. Yovine, Building models of real-time systems from application software, Proc. of the IEEE, vol.91, issue.1, pp.100-111, 2003.

A. P. Sistla, Safety, liveness and fairness in temporal logic, Formal Asp. Comput, vol.6, issue.5, pp.495-512, 1994.

D. Song, J. Lettner, P. Rajasekaran, Y. Na, S. Volckaert et al., Sok: Sanitizing for security, 2018.

L. Szekeres, M. Payer, T. Wei, and D. Song, Sok: Eternal war in memory, 2013 IEEE Symp, pp.48-62, 2013.

C. Talhi, N. Tawbi, and M. Debbabi, Execution monitoring enforcement under memorylimitation constraints, Inf. Comput, vol.206, issue.2-4, pp.158-184, 2008.

M. Wu, H. Zeng, and C. Wang, Synthesizing runtime enforcer of safety properties under burst error, NASA Formal Methods -8th Int. Symp. LNCS, vol.9690, pp.65-81, 2016.

M. Wu, H. Zeng, C. Wang, and H. Yu, Safety guard: Runtime enforcement for safety-critical cyber-physical systems: Invited, Proc. of the 54th Annual Design Automation Conf. pp, vol.84, pp.1-84, 2017.

X. Yin and S. Lafortune, A new approach for synthesizing opacity-enforcing supervisors for partially-observed discrete-event systems, American Control Conf., ACC 2015, pp.377-383, 2015.

X. Zhang, M. Leucker, and W. Dong, Runtime verification with predictive semantics, NASA Formal Methods -4th Int. Symp, vol.7226, pp.418-432, 2012.