Publications

For authors: Please add “This article is based upon work from COST Action ARVI IC1402, supported by COST (European Cooperation in Science and Technology).” to acknowledge the support by COST.

2018

  • Piergiuseppe Mallozzi, Raúl Pardo, Vincent Duplessis, Patrizio Pelliccione, and Gerardo Schneider. MoVEMo: A Structured Approach for Engineering Reward Functions. In Second IEEE International Conference on Robotic Computing (IRC’18), pages 250-257. IEEE Computer Society, 2018
  • Srinivas Pinisetty, David Sands, and Gerardo Schneider. Runtime Verification of Hyperproperties for Deterministic Programs. In 6th Conference on Formal Methods in Software Engineering (FormaliSE@ICSE’18), pages 20-29. ACM, 2018
  • Raúl Pardo, César Sánchez, and Gerardo Schneider. Timed Epistemic Knowledge Bases for Social Networks. In Formal Methods (FM’18), volume 10951 of LNCS, pages 185-202. Springer, 2018.
  • Borzoo Bonakdarpour, César Sánchez, and Gerardo Schneider. Monitoring Hyperproperties by Combining Static Analysis and Runtime Verification. In 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation – Track: A Broader View on Verification: From Static to Runtime and Back (ISoLA’18, part II), volume 11245 of LNCS, pages 8-27. Springer, 2018.
  • João M. Lourenço, Jan Fiedor, Bohuslav Krena, Tomás Vojnar:
    Discovering Concurrency Errors. Lectures on Runtime Verification 2018: 34-60
  • Ricardo J. Dias, Carla Ferreira, Jan Fiedor, João M. Lourenço, Ales Smrcka, Diogo G. Sousa, Tomás Vojnar:
    Verifying Concurrent Programs Using Contracts. ICST 2017: 196-206
  • Yliès Falcone, César Sánchez:
    Introduction to the special issue on runtime verification. Formal Methods in System Design 53(1): 1-5 (2018)
  • Sylvain Hallé, Raphaël Khoury, Quentin Betti, Antoine El-Hokayem, Yliès Falcone:
    Decentralized enforcement of document lifecycle constraints. Inf. Syst. 74(Part): 117-135 (2018)
  • Simone Silvetti, Laura Nenzi, Ezio Bartocci, Luca Bortolussi, Signal Convolution Logic, Proc. of ATVA 2018: the 16th International Symposium on Automated Technology for Verification and Analysis, LNCS, to appear, 2018
  • Laura Nenzi, Simone Silvetti, Ezio Bartocci, Luca Bortolussi, A Robust Genetic Algorithm for Learning Temporal Specifications from Data, Proc. of QEST 2018: the 15th International Conference on Quantitative Evaluation of SysTems, LNCS, vol. 11024, pp. 323–338, 2018
  • Ezio Bartocci, Roderick Bloem, Dejan Nickovic, Franz Roeck, A Counting Semantics for Monitoring LTL Specifications over Finite Traces, Proc. of CAV 2018: the 30th International Conference on Computer-Aided Verification, Springer, LNCS, vol. 10981, pp. 547-564, 2018
  • Ezio Bartocci, Yliès Falcone, Adrian Francalanza, Giles Reger, Introduction to Runtime Verification, Lectures on Runtime Verification 2018, LNCS, vol. 10457, pp. 1-33, Springer
  • Ezio Bartocci, Jyotirmoy V. Deshmukh, Alexandre Donzé, Georgios E. Fainekos, Oded Maler, Dejan Nickovic, Sriram Sankaranarayanan,Specification-Based Monitoring of Cyber-Physical Systems: A Survey on Theory, Tools and Applications, Lectures on Runtime Verification 2018 , LNCS, vol. 10457, pp. 135-175, Springer
  • Stefan Jaksic, Ezio Bartocci, Radu Grosu, Thang Nguyen, Dejan Nickovic, Quantitative Monitoring of STL with Edit Distance, In Journal Formal Methods in Systems Design, (In press) , 2018
  • Ezio Bartocci, T. Ferrère, Niveditha Manjunath, Dejan Nickovic, Localizing Faults in Simulink/Stateflow Models with Signal Temporal Logic, In Proc. of HSCC 2018: the 21st ACM International Conference on Hybrid Systems: Computation and Control, pp. 197-206, ACM, 2018
  • Ezio Bartocci, Yliès Falcone, Lectures on Runtime Verification – Introductory and Advanced Topics, Lecture Notes in Computer Science 10457, Springer 2018, ISBN 978-3-319-75631-8
  • Rimantas Seinauskas, The Examination of Shall Be Impossible Situations for Verification During Execution, American Journal of Computer Science and Technology. Vol. 1, No. 2, 2018, pp. 44-54. doi: 10.11648/j.ajcst.20180102.12

2017

  • Hosein Nazarpour, Yliès Falcone, Saddek Bensalem, Marius Bozga:
    Concurrency-preserving and sound monitoring of multi-threaded component-based systems: theory, algorithms, implementation, and evaluation. Formal Asp. Comput. 29(6): 951-986 (2017)
  • Ferruccio Damiani, David Faitelson, Christoph Gladisch, Shmuel S. Tyszberowicz.
    A novel model-based testing approach for software product lines. Software and System Modeling 16(4): 1223-1251 (2017)
  • Ali Kassem, Yliès Falcone, Pascal Lafourcade:
    Formal analysis and offline monitoring of electronic exams. Formal Methods in System Design 51(1): 117-153 (2017)
  • Srinivas Pinisetty, Viorel Preoteasa, Stavros Tripakis, Thierry Jéron, Yliès Falcone, Hervé Marchand:
    Predictive runtime enforcement. Formal Methods in System Design 51(1): 154-199 (2017)
  • Srinivas Pinisetty, Thierry Jéron, Stavros Tripakis, Yliès Falcone, Hervé Marchand, Viorel Preoteasa:
    Predictive runtime verification of timed properties. Journal of Systems and Software 132: 353-365 (2017)
  • Yliès Falcone, Mohamad Jaber:
    Fully automated runtime enforcement of component-based systems with formal and sound recovery. STTT 19(3): 341-365 (2017)
  • Raphaël Jakse, Yliès Falcone, Jean-François Méhaut, Kevin Pouget:
    Interactive Runtime Verification – When Interactive Debugging Meets Runtime Verification. ISSRE 2017: 182-193
  • Antoine El-Hokayem, Yliès Falcone:
    Monitoring decentralized specifications. ISSTA 2017: 125-135
  • Antoine El-Hokayem, Yliès Falcone:
    THEMIS: a tool for decentralized monitoring algorithms. ISSTA 2017: 372-375
  • Ezio Bartocci, Rupak Majumdar: Introduction to the special issue on runtime verification. Formal Methods in System Design 51(1): 1-4 (2017)
  • Matthieu Renard, Antoine Rollet, Yliès Falcone:
    GREP: Games for the Runtime Enforcement of Properties. ICTSS 2017: 259-275
  • Oliviero Riganelli, Daniela Micucci, Leonardo Mariani, Yliès Falcone:
    Verifying Policy Enforcers. RV 2017: 241-258
  • Matthieu Renard, Antoine Rollet, Yliès Falcone:
    Runtime enforcement using Büchi games. SPIN 2017: 70-79
  • Ezio Bartocci, Ylies Falcone, Borzoo Bonakdarpour, Christian Colombo, Normann Decker, Felix Klaedtke, Klaus Havelund, Yogi Joshi, Reed Milewicz, Giles Reger, Grigore Rosu, Julien Signoles, Daniel Thoma, Eugen Zalinescu, Yi Zhang,
    First International Competition on Runtime Verification, Rules, Benchmarks, Tools, and Final Results of CRV 2014.     In Journal of Software Tools for Technology Transfer, (in press), 2017
  • Ezio Bartocci, Luca Bortolussi, Michele Loreti, Laura Nenzi
    Monitoring Mobile and Spatially Distributed Cyber-Physical Systems In Proc. of MEMOCODE 2017: the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, ACM, pp. 146–155, 2017
  • Konstantin Selyunin, Stefan Jaksic, Thang Nguyen, C. Reidl, U. Hafner, Ezio Bartocci, Dejan Nickovic, Radu Grosu, Runtime Monitoring with Recovery of the SENT Communication Protocol In Proc. of CAV 2017: the 29th International Conference on Computer-Aided Verification, Springer, Lecture Notes in Computer Science, vol. 10426, pp. 336–355, 2017
  • Houssam Abbas, Alena Rodionova, Ezio Bartocci, Scott A. Smolka, Radu Grosu, Quantitative Regular Expressions for Arrhythmia Detection Algorithms In Proc. of CMSB 2017: the 15th International Conference on Computational Methods in Systems Biology, Springer Berlin Heidelberg, Lecture Notes in Computer Science, vol. 10545, pp. 23–39, 2017

2016

  • Andreas Bauer, Yliès Falcone:
    Decentralised LTL monitoring. Formal Methods in System Design 48(1-2): 46-93 (2016)
  • Sylvain Hallé, Raphaël Khoury, Antoine El-Hokayem, Yliès Falcone:
    Decentralized Enforcement of Artifact Lifecycles. EDOC 2016: 1-10
  • Hosein Nazarpour, Yliès Falcone, Saddek Bensalem, Marius Bozga, Jacques Combaz:
    Monitoring Multi-threaded Component-Based Systems. IFM 2016: 141-159
  • Ezio Bartocci, Rupak Majumdar, Introduction to the special issue on runtime verification. Formal Methods in System Design 51(1): 1-4 (2017)
  • Dilian Gurov, Klaus Havelund, Marieke Huisman, Rosemary Monahan, Static and Runtime Verification, Competitors or Friends? (Track Summary). In 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation – ISoLA’16 (1), volume 9952 of LNCS, pages 397 – 401. Springer, 10-14 October 2016.
  • Christian Colombo and Ylies Falcone, Organising LTL Monitors over Distributed Systems with a Global Clock, in Formal Methods in System Design, 49(1-2): 109-158, 2016.
  • Christian Colombo and Yliès Falcone, First International Summer School on Runtime Verification – As Part of the ArVi COST Action 1402, Runtime Verification, volume 10012 of LNCS, pages 17-20, 2016.
  • Gordon Pace, Raúl Pardo, and Gerardo Schneider. On the Runtime Enforcement of Evolving Privacy Policies in Online Social Networks. In 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation – ISoLA’16 (2); Track: Runtime Verification and Enforcement, the (industrial) application perspective, volume 9953 of LNCS, pages 407-412. Springer, 10-14 October 2016.
  • Gerardo Schneider. On the Specification and Enforcement of Privacy-Preserving Contractual Agreements. In 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation – ISoLA’16 (2); Track: Runtime Verification and Enforcement, the (industrial) application perspective, volume 9953 of LNCS, pages 413-419. Springer, 10-14 October 2016.
  • Shaun Azzopardi, Gordon J. Pace, Fernando Schapachnik, and Gerardo Schneider. Contract Automata: An Operational View of Contracts Between Interactive Parties. Artificial Intelligence and Law, 24(3):203-243, September 2016.
  • Raúl Pardo, Ivana Kellyérová, César Sánchez, and Gerardo Schneider. Specification of Evolving Privacy Policies for Online Social Networks. In 23rd International Symposium on Temporal Representation and Reasoning (TIME’16), pages 70-79. IEEE CPS, 2016.
  • Raúl Pardo, Christian Colombo, Gordon Pace, and Gerardo Schneider. An Automata-based Approach to Evolving Privacy Policies for Social Networks. In The 16th International Conference on Runtime Verification (RV’16), volume 10012 of LNCS, pages 285-301. Springer, 2016.
  • Ezio Bartocci, Thang Nguyen, Radu Grosu, Stefan Jaksic, Dejan Nickovic, Konstantin Selyunin, The HARMONIA project: Hardware Monitoring for Automotive Systems-of-Systems, In Proc. of ISoLA 2016: the 7th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, Springer, Lecture Notes in Computer Science, 2016, to appear
  • Ezio Bartocci, Ylies Falcone, Runtime Verification and Enforcement, the (Industrial) Application Perspective (Track Introduction), In Proc. of ISoLA 2016: the 7th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, Springer, Lecture Notes in Computer Science, 2016, to appear
  • Konstantin Selyunin, Thang Nguyen, Ezio Bartocci, Radu Grosu, Applying Runtime Monitoring for Automotive Electronic Development, In Proc. of RV 2016: the 7th International Conference on Runtime Verification, Springer, Lecture Notes in Computer Science, 2016, to appear
  • Stefan Jaksic, Ezio Bartocci, Radu Grosu, Dejan Nickovic, Quantitative Monitoring of STL with Edit Distance, In Proc. of RV 2016: the 7th International Conference on Runtime Verification, Springer, Lecture Notes in Computer Science, 2016, to appear
  • Konstantin Selyunin, Thang Nguyen, Ezio Bartocci, Dejan Nickovic, Radu Grosu, Monitoring of MTL Specifications With IBM’s Spiking-Neuron Model, In Proc. of DATE 2016: the 2016 Design, Automation & Test in Europe Conference & Exhibition, IEEE Computer Society, pp. 924-929, 2016
  • Ezio Bartocci, Ebru Aydin-Gol, Iman Haghighi, Calin Belta, A Formal Methods Approach to Pattern Recognition and Synthesis in Reaction Diffusion Networks, accepted in IEEE Transactions on Control of Network Systems, (in press), 2016
  • Ezio Bartocci, Luca Bortolussi, Tomas Brazdil, Dimitrios Milios, Guido Sanguinetti, Policy learning for time-bounded reachability in Continuous-Time Markov Decision Processes via doubly-stochastic gradient ascent, In Proc. of QEST 2016: the 13th International Conference on Quantitative Evaluation of SysTems, Springer, Lecture Notes in Computer Science, vol. 9826, pp. 244–259, 2016
  • Alena Rodionova, Ezio Bartocci, Dejan Nickovic, Radu Grosu, Temporal Logic as Filtering. In Proc. of HSCC’16: the 19th International Conference on Hybrid Systems: Computation and Control, pp. 11-20, ACM, 2016 (Best Student Runner-up Paper Award)
  • Antoine El-Hokayem, Yliès Falcone, and Mohamad Jaber.
    Modularizing Crosscutting Concerns in Component-Based Systems.
    In SEFM 2016: 14th International Conference on
    Software Engineering and Formal Methods. Pre-print. To appear.
  • Normann Decker, Jannis Harder, Torben Scheffel, Malte Schmitz, Daniel
    Thoma: Runtime Monitoring with Union-Find Structures. In Marsha Chechik,
    Jean-François Raskin (Eds.): International Conference on Tools and
    Algorithms for the Construction and Analysis of Systems, International
    Conference, TACAS 2016, LNCS 9636, Springer (2016).
  • Hosein Nazarpour, Yliès Falcone, Saddek Bensalem, Marius Bozga, Jacques Combaz. Monitoring Multi-threaded Component-based Systems.
    In Proc. of iFM 2016, the 12th international conference on integrated Formal Methods. To Appear. Pre-print.
  • Yliès Falcone, Thierry Jéron, Hervé Marchand, Srinivas Pinisetty. Runtime enforcement of regular timed properties by suppressing and delaying events.
    In SCP: Science of Computer Programming. Pre-print. Online editor version.

2015

  • Ezio Bartocci, Luca Bortolussi, Laura Nenzi, Guido Sanguinetti, System Design of Stochastic Models using Robustness of Temporal Properties. In Theoretical Computer Science, vol. 587, pp. 3-25, 2015
  • Stefan Jaksic, Ezio Bartocci, Radu Grosu, Reinhard Kloibhofer, Thang Nguyen, Dejan Nickovic, From Signal Temporal Logic to FPGA Monitors. In Proc. of MEMOCODE 2015: the 13th ACM-IEEE International Conference on Formal Methods and Models for System Design, ACM, pp. to appear, 2015
  • Ezio Bartocci, Luca Bortolussi, Dimitrios Milios, Laura Nenzi, Guido Sanguinetti, Studying Emergent Behaviours in Morphogenesis using Signal Spatio-Temporal Logic. In Proc. of HSB 15: the 4th International Workshop on Hybrid Systems Biology, LNCS, vol. , pp. to Appear, 2015
  • Giles Reger and David E. Rydeheard. From First-order Temporal Logic to Parametric Trace Slicing. In Proc. of RV 15: the 15th International Conference on Runtime Verification, pp. 216-232, 2015
  • Matthieu Renard, Yliès Falcone, Antoine Rollet, Srinivas Pinisetty, Thierry Jéron, Hervé Marchand. Enforcement of (Timed) Properties with Uncontrollable Events. ICTAC 2015, LNCS, pp. 542-560, 2015. Pre-print.
  • Ali Kassem, Yliès Falcone, Pascal Lafourcade. Monitoring Electronic Exams. RV 2015, LNCS, pp. 118-135, 2015. Pre-print.
  • Srinivas Pinisetty, Yliès Falcone, Thierry Jéron, Hervé Marchand. TiPEX: A Tool Chain for Timed Property Enforcement During eXecution. RV 2015, LNCS, pp. 306-320, 2015. Pre-print.
  • Yliès Falcone, Dejan Nickovic, Giles Reger, Daniel Thoma. Second International Competition on Runtime Verification CRV 2015. RV 2015, LNCS, pp. 405-422, 2015. Pre-print.