Publications

Under Submission

• Position: A Three-Layer Probabilistic Assume-Guarantee Architecture Is Structurally Required for Safe LLM Agent Deployment
  S.Bensalem, Y. Dong, M. Franzle, X. Huang, J. Kroger, D. Nickovic, A. Nouri, R. Roy, C. Wu
  arXiv

• PrefixGuard: From LLM-Agent Traces to Online Failure-Warning Monitors
  X. Huang, J. Hu, R. Roy, C. Wu, Y. Dong, X. Huang
  arXiv

Conference Papers

• About Time: Model-free Reinforcement Learning with Timed Reward Machines
  A. Majumdar, R. Raha, R. Roy, D. Parker, M. Kwiatkowska
  IJCAI-ECAI 2026: To appear
  tool arXiv

• Learning Probabilistic Temporal Logic Specifications for Stochastic Systems
  R. Roy, Y. Pote, D. Parker, M. Kwiatkowska
  IJCAI 2025: International Joint Conference on Artificial Intelligence, 2025
  paper tool arXiv

• The Complexity of Learning LTL, CTL and ATL formulas
  B. Bordais, D. Neider, R. Roy.
  STACS 2025: Symposium on Theoretical Aspects of Computer Science, 2025
  paper

• What Is Formal Verification Without Specifications? A Survey on Mining LTL Specifications
  D. Neider, R. Roy.
  POV 2025: Principles of Verification: Cycling the Probabilistic Landscape, 2025
  paper

• Learning Branching-Time Properties in CTL and ATL via Constraint Solving
  B. Bordais, D. Neider, R. Roy.
  FM 2024: Formal Methods, 2024
  paper tool

• Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic.
  R. Raha, R. Roy, N. Fijalkow, D. Neider, G.A. Perez.
  VMCAI 2024: Verification, Model Checking, and Abstract Interpretation, 2024
  paper tool

• Specification Sketching for Linear Temporal Logic.
  S. Lutz, D. Neider, R. Roy.
  ATVA 2023: Automated Technology For Verification and Analysis, 2023
  paper tool arXiv

• Reinforcement Learning with Temporal-Logic-Based Causal Diagrams.
  Y. Paliwal, R. Roy, J. Gaglione, N. Baharisangari, D. Neider, Xiaoming Duan, U. Topcu, Z. Xu.
  CD-MAKE 2023: Cross Domain Conference for Machine Learning and Knowledge Extraction, 2023
  paper arXiv

• Learning Interpretable Temporal Properties from Positive Examples Only.
  R. Roy, J. Gaglione, N. Baharisangari, D. Neider, U. Topcu, Z. Xu.
  AAAI 2023: AAAI Conference on Artificial Intelligence, 2023
  paper arXiv poster talk

• Analyzing Robustness of Angluin’s L* Algorithm in Presence of Noise.
  I. Khmelnitsky, S. Haddad, L. Ye, B. Barbot, B. Bollig, M. Leucker, D. Neider, R. Roy.
  GandALF 2022: Games, Automata, Logics and Formal Verification, 2022
  paper

• Robust Computation Tree Logic.
  S.P. Nayak, D. Neider, R. Roy, M. Zimmerman.
  NFM 2022: NASA Formal Methods Symposium, 2022
  paper arXiv

• Scalable Anytime Algorithms for Learning Fragments of Linear Temporal Logic.
  R. Raha, R. Roy, N. Fijalkow, D. Neider.
  TACAS 2022: Tools and Algorithms for the Construction and Analysis of Systems, 2022
  paper arXiv tool poster

• Extracting Context-Free Grammars from Recurrent Neural Networks using Tree-Automata Learning and A* Search.
  B. Barbot, B. Bollig, A. Finkel, S. Haddad, I. Khmelnitsky, M. Leucker, D. Neider, R. Roy, L. Ye.
  ICGI 2021: International Conference on Grammatical Inference, 2021
  paper talk

• Learning Linear Temporal Properties from Noisy Data - A MaxSAT-based approach.
  J. Gaglione, D. Neider, R. Roy, U. Topcu, Z. Xu.
  ATVA 2021: Automated Technology For Verification and Analysis, 2021
  paper arXiv tool talk

• Property-Directed Verification and Robustness Certification of Recurrent Neural Networks.
  I. Khmelnitsky, D. Neider, R. Roy, X. Xie, B. Barbot, B. Bollig, A. Finkel, S. Haddad, M. Leucker, L. Ye.
  ATVA 2021: Automated Technology For Verification and Analysis, 2021
  paper arXiv repository

• Quality Guarantees for Autoencoders via Unsupervised Adversarial Attacks.
  B. Böing, R. Roy, E. Müller, D. Neider.
  ECML/PKDD 2020: Machine Learning and Knowledge Discovery in Databases - European Conference, 2020
  paper open-access talk

• Learning Interpretable Models in the Property Specification Language.
  R. Roy, D. Fisman, D. Neider.
  IJCAI 2020: International Joint Conference on Artificial Intelligence, 2021
  paper talk poster

• On Verifying TSO Robustness for Event-Driven Asynchronous Programs.
  A. Bouajjani, C. Enea, M. Mukund, R. Roy.
  NETYS 2018: Networked Systems - 6th International Conference, 2018
  paper

Journal and Workshop Papers

• SCARLET: Scalable Anytime Algorithms for Learning Fragments of Linear Temporal Logic.
  R. Raha, R. Roy, N. Fijalkow, D. Neider.
  JOSS 2024: Journal of Open Source Software, 2024
  paper

• Analyzing Robustness of Angluin’s L* Algorithm in Presence of Noise.
  I. Khmelnitsky, S. Haddad, L. Ye, B. Barbot, B. Bollig, M. Leucker, D. Neider, R. Roy.
  LMCS 2024: Logical Methods in Computer Science, 2024
  paper

• Analysis of Recurrent Neural Networks via Property-Directed Verification of Surrogate Models
  I. Khmelnitsky, D. Neider, R. Roy, X. Xie, B. Barbot, B. Bollig, A. Finkel, S. Haddad, M. Leucker, L. Ye.
  STTT 2022: International Journal on Software Tools for Technology Transfer, 2022
  paper

• Expanding the horizon of Linear Temporal Logic Inference for Explainability
  R. Roy, D. Neider.
  RE4ES 2022: Requirements Engineering for Explainable Systems, 2022
  paper

• MaxSAT-based Temporal Logic Inference from Noisy Data
  J. Gaglione, D. Neider, R. Roy, U. Topcu, Z. Xu.
  ISSE 2022: Innovations in Systems and Software Engineering, 2022
  paper

• QUGA - Quality Guarantees for Autoencoders.
  B. Böing, R. Roy, E. Müller, D. Neider.
  OVERLAY@GandALF 2021: Artificial Intelligence and fOrmal VERification, Logic, Automata, and sYnthesis, 2021
  paper

Thesis

• PhD thesis: Learning Temporal Properties for Explainability and Verification
  pdf link

• Master’s thesis: SAT-based learning algorithms.
  pdf

Tools

• SCARLET: A scalable LTL inference tool.
  website github package

• Flie-PSL: A tool for inferring PSL formulas.
  github