Symbolic optimal expected time reachability computation and controller synthesis for probabilistic timed automata. - Aleksandra Jovanovic 002; Marta Kwiatkowska; Gethin Norman; Quentin Peyras (Theor. Comput. Sci., 2017)

A Bounded Domain Property for an Expressive Fragment of First-Order Linear Temporal Logic. - Quentin Peyras; Julien Brunel; David Chemouil (TIME, 2019)

Sound Verification Procedures for Temporal Properties of Infinite-State Systems. - Quentin Peyras; Jean-Paul Bodeveix; Julien Brunel; David Chemouil (CAV (2), 2021)

A decidable and expressive fragment of Many-Sorted First-Order Linear Temporal Logic. - Quentin Peyras; Julien Brunel; David Chemouil (Inf. Comput., 2021)

Towards Verifying Security Policies for Infinite-State Systems. - Quentin Peyras; Ghada Gharbi; Souheib Baarir (VSTTE, 2024)