, Interactive Runtime Verification: Formal Models, Algorithms, and Implementation, 2031.

, Lectures on Runtime Verification -Introductory and Advanced Topics, Lecture Notes in Computer Science, vol.10457, 2018.

M. Brörkens and M. Möller, Dynamic Event Generation for Runtime Checking using the JDI, Electr. Notes Theor. Comput. Sci, vol.70, pp.80575-80584, 2002.

D. Bruening and Q. Zhao, Practical memory checking with Dr. Memory, The 9th International Symposium on Code Generation and Optimization, pp.213-223, 2011.

D. Bruening, Q. Zhao, and S. P. Amarasinghe, Transparent dynamic instrumentation, Proceedings of the 8th International Conference on Virtual Execution Environments, VEE 2012, 2012.

, , pp.133-144

M. Chabot, K. Mazet, and L. Pierre, Automatic and configurable instrumentation of C programs with temporal assertion checkers, ACM/IEEE International Conference on Formal Methods and Models for Codesign, vol.13, pp.208-217, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01393418

F. Chen and G. Rosu, Mop: an efficient and generic runtime verification framework, Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2007, pp.569-588, 2007.

F. Chen and G. Rosu, Parametric Trace Slicing and Monitoring, Tools and Algorithms for the Construction and Analysis of Systems, 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, pp.246-261, 2009.

Y. Cheon and G. T. Leavens, A Simple and Practical Approach to Unit Testing: The JML and JUnit Way, ECOOP 2002 -Object-Oriented Programming, 16th European Conference, pp.231-255, 2002.

E. M. Clarke, O. Grumberg, and D. A. Peled, Model checking, 2001.

C. Colombo, A. Francalanza, and R. Gatt, Elarva: A Monitoring Tool for Erlang, Runtime Verification -Second International Conference, vol.7186, pp.370-374, 2011.

P. Cousot and R. Cousot, Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints, Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, pp.238-252, 1977.

P. Cuoq, F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles et al., Frama-C -A Software Analysis Perspective, Software Engineering and Formal Methods -10th International Conference, SEFM 2012, vol.7504, pp.233-247, 2012.

Q. B. Fabio and . Da-silva, Correctness proofs of compilers and debuggers : an approach based on structural operational semantics, 1992.

M. Ducassé and E. Jahier, Efficient Automated Trace Analysis: Examples with Morphine, Electr. Notes Theor. Comput. Sci, vol.55, pp.248-256, 2001.

M. Ducassé, Opium: an extendable trace analyzer for Prolog, The Journal of Logic Programming, vol.39, pp.10036-10041, 1999.

E. , A. Emerson, and E. M. Clarke, Characterizing Correctness Properties of Parallel Programs Using Fixpoints, Automata, Languages and Programming, 7th Colloquium, Noordweijkerhout, The Netherland, vol.85, pp.169-181, 1980.

J. E. , A review of reverse debugging, System, Software, SoC and Silicon Debug Conference (S4D), pp.1-6, 2012.

Y. Falcone, You Should Better Enforce Than Verify, Runtime Verification -First International Conference, RV 2010, St. Julians, Malta, vol.6418, pp.89-105, 2010.
URL : https://hal.archives-ouvertes.fr/hal-00523653

K. Georgiev and V. Marangozova-martin, MPSoC Zoom Debugging: A Deterministic Record-Partial Replay Approach, 12th IEEE International Conference on Embedded and Ubiquitous Computing, pp.73-80, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01006231

K. Havelund and A. Goldberg, Verify Your Runs, Verified Software: Theories, Tools, Experiments, First IFIP TC 2/WG 2.3 Conference, vol.4171, pp.374-383, 2005.

J. Itkonen, V. Mika, C. Mäntylä, and . Lassenius, Defect detection efficiency: Test case based vs. exploratory testing, First International Symposium on Empirical Software Engineering and Measurement, pp.61-70, 2007.

J. Itkonen, V. Mika, C. Mantyla, and . Lassenius, How do testers do it? An exploratory study on manual testing practices, Proceedings of the 3rd International Symposium on Empirical Software Engineering and Measurement, pp.494-497, 2009.

R. Jakse, Y. Falcone, J. Méhaut, and K. Pouget, Interactive Runtime Verification -When Interactive Debugging Meets Runtime Verification, 28th IEEE International Symposium on Software Reliability Engineering, pp.182-193, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01592671

R. Jakse, Y. Falcone, and J. Méhaut, , 2017.

D. Jin, O. Patrick, C. Meredith, G. Lee, and . Rosu, JavaMOP: Efficient parametric runtime monitoring framework, 34th International Conference on Software Engineering, ICSE 2012, pp.1427-1430, 2012.

S. Katz, Chapter Aspect Categories and Classes of Temporal Properties, Transactions on Aspect-Oriented Software Development I, pp.106-134, 2006.

G. Kiczales, AspectJ(tm): Aspect-Oriented Programming in Java, Objects, Components, Architectures, Services, and Applications for a Networked World, International Conference NetObjectDays, vol.2591, 2002.

M. Leucker and C. Schallhart, A brief account of runtime verification, J. Log. Algebr. Program, vol.78, pp.293-303, 2009.

C. Luk, R. S. Cohn, R. Muth, H. Patil, A. Klauser et al., Pin: building customized program analysis tools with dynamic instrumentation, Proceedings of the ACM SIGPLAN, 2005.

, Conference on Programming Language Design and Implementation, pp.190-200, 2005.

R. Milewicz, R. Vanka, J. Tuck, D. Quinlan, and P. Pirkelbauer, Lightweight runtime checking of C programs with RTC. Computer Languages, Systems & Structures, vol.45, pp.191-203, 2016.

R. Milner, Communication and concurrency, 1989.

S. Navabpour, Y. Joshi, C. Wu, S. Berkovich, R. Medhat et al., RiTHM: a tool for enabling time-triggered runtime verification for C programs, Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE'13, pp.603-606, 2013.

N. Nethercote and J. Seward, Valgrind: a framework for heavyweight dynamic binary instrumentation, Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, pp.89-100, 2007.

F. Petrillo, Z. Soh, F. Khomh, M. Pimenta, C. M. Freitas et al., Towards Understanding Interactive Debugging, 2016 IEEE International Conference on Software Quality, Reliability and Security, QRS 2016. IEEE, pp.152-163, 2016.

K. Pouget, Programming-Model Centric Debugging for multicore embedded systems / Debogage Interactif des systemes embarques multicoeur base sur le model de programmation, 2014.
URL : https://hal.archives-ouvertes.fr/tel-01010061

N. Ramsey, Correctness of Trap-Based Breakpoint Implementations, Conference Record of POPL'94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.15-24, 1994.

J. Roos, L. Courtrai, and J. Méhaut, Execution replay of parallel programs, Euromicro Workshop on Parallel and Distributed Processing, pp.429-434, 1993.

O. Sokolsky, K. Havelund, and I. Lee, Introduction to the special section on runtime verification, International Journal on Software Tools for Technology Transfer, vol.14, pp.243-247, 2012.

, Breakpoint 2, queue_push (q=0x5...59260, c=101 'e') at faulty.c, p.30

, Num Type Disp Enb Address What 53 2 breakpoint keep y 0x00005...55233 in queue_push at faulty, p.30

, Reading symbols from

, Breakpoint 1 at 0x1380: file faulty.c, line 52

, Temporary breakpoint 2 at 0x1372: file faulty.c, line 51

, Temporary breakpoint, vol.2, p.51

, double_queue_t * q = queue_init(

, at faulty.c:52 70 52 queue_push_str(q

, Event: queue_new{'size': 16, 'queue

, Slice 1 <None>: init (from init)

, Slice 2 <93824992252512>: queue_ready

, Slice 2 <93824992252512>: queue_ready (from queue_ready) 24 N: 1 25 max: 16 27 Event: queue_push{'queue

, Slice 2 <93824992252512>: queue_ready (from queue_ready)

, Slice 2 <93824992252512>: queue_ready (from queue_ready)

, Event: queue_push{'queue, p.93824992252512