Towards Proved Formal Specification and Verification of STL Operators as Synchronous Observers. - Céline Bellanger; Pierre-Loïc Garoche; Matthieu Martel; Célia Picard (FMAS@iFM, 2023)

Formally proved specification of non-nested STL formulas as synchronous observers. - Céline Bellanger; Pierre-Loïc Garoche; Matthieu Martel; Célia Picard (Sci. Comput. Program., 2025)