Professional homepage of Thomas Ferrère

Senior Hardware Engineer, Imagination Technologies.

Research

Datapath design
Computer arithmetic
Runtime verification
Embedded systems

News

Symposium on Computer Arithmetic ARITH 2022.
Federated Logic Conference FLOC 2022.

Short CV

I am a senior hardware engineer at Imagination Technologies, Kings Langley, UK. Previously, I was postdoctoral researcher at IST Austria, Klosterneuburg, Austria in the group of Thomas A. Henzinger. I completed my PhD at Verimag, University of Grenoble, France under the supervision of Oded Maler and in collaboration with Mentor Graphics corporation.

Previous Events

RV 2021 (committee member)
RV 2020 (committee member)
DARS 2019 (committee member)
RV4RISE 2018 (invited speaker)
FAC 2018 (program co-chair, with Dejan Nickovic)
DARS 2018 (program co-chair, with Sicun Gao)
EQINOCS 2016 (invited speaker)
MTCPS 2016 (committee member)

PhD Thesis

Assertions and Measurements for Mixed-Signal Simulation, University of Grenoble, 2016.

Publications

Preprints by topic. See also DBLP and Google Scholar. Copyright belongs to respective publishers.

Monitorability
We defined automata models capturing the (online) monitorability of discrete languages beyond finite-state. We invented a strongly convergent algorithm to monitor the frequency of Markov-distributed events.
- A Theory of Register Monitors.
  LICS paper with Thomas A. Henzinger and N. Ege Sarac (2018).
- Monitoring Event Frequencies.
  CSL paper with Thomas A. Henzinger and Bernhard Kragl (2020).
Real-time Logics
We extended a result on the decidability of real-time temporal logic, based on infinitely precise semantics and finitely precise syntax. We studied the (offline) monitoring of temporal logic extended with clock variables or mixed discrete-/continuous-time modalities. We proposed an algorithm to monitor a first-order logic with real-valued variables, in which properties such as eventual stability can be described.
- From Real-time Logic to Timed Automata.
  JACM paper with Oded Maler, Dejan Nickovic and Amir Pnueli (2019).
- The Compound Interest in Relaxing Punctuality.
  FM paper (2018).
- Monitoring Temporal Logic with Clock Variables.
  FORMATS paper with Adrian Elgyutt and Thomas A. Henzinger (2018).
- Mixed-Time Signal Temporal Logic.
  FORMATS paper with Oded Maler and Dejan Nickovic (2019).
- The First Order Logic of Signals.
  EMSOFT invited paper with Alexey Bakhirkin, Thomas A. Henzinger and Dejan Nickovic (2018).
Robust Monitoring
We invented an efficient algorithm to compute the continuous satisfaction degree (robustness) of a temporal formula over real-valued signals. We proposed a variant of this algorithm to perform parametric identification. We redefined the continuous satisfaction degree according to a system's interface and showed that resulting notions of vacuity and robustness simplify the falsification problem.
- Efficient Robust Monitoring for STL.
  CAV paper with Alexandre Donzé and Oded Maler (2013).
- Efficient Parametric Identification for STL.
  HSCC paper with Alexey Bakhirkin and Oded Maler (2018).
- Interface-Aware Signal Temporal Logic.
  HSCC paper with Dejan Nickovic, Alexandre Donzé, Hisahiro Ito and James Kapinski (2019).
Fault Localization
We demonstrated how segments of a signal falsifying a given formula can be identified. We combined this analysis with formal and statistical techniques to accelerate the localisation of faults in a white-box system.
- Trace Diagnostics using Temporal Implicants.
  ATVA paper with Oded Maler and Dejan Nickovic (2015).
- Localizing Faults in Simulink/Stateflow Models with STL.
  HSCC paper with Ezio Bartocci, Niveditha Manjunath and Dejan Nickovic (2018).
Pattern Matching
We invented an offline algorithm to match regular expressions over continuous signals. We adapted this algorithm to operate online through the notions of regular expression derivatives and timed automata. We associated regular expressions over real-valued signals with an (offline-computable) contiuous satisfaction degree.
- Timed Pattern Matching.
  FORMATS paper with Dogan Ulus, Eugene Asarin and Oded Maler (2014).
- Online Timed Pattern Matching using Derivatives.
  TACAS paper with Dogan Ulus, Eugene Asarin and Oded Maler (2016).
- Online Timed Pattern Matching using Automata.
  FORMATS paper with Alexey Bakhirkin, Dejan Nickovic, Oded Maler and Eugene Asarin (2018).
- On the Quantitative Semantics of Regular Expressions over Real-Valued Signals.
  FORMATS paper with Alexey Bakhirkin, Oded Maler and Dogan Ulus (2017).
Pattern Measuring
We demonstrated how to use regular patterns to specify and extract measurements over real-valued signals: firstly, by associating each matched segment with an aggregation function such as average or min/max; secondly, by decomposing the matched segment into a series of basic shapes through statistical regression.
- Measuring with Timed Patterns.
  CAV paper with Oded Maler, Dejan Nickovic and Dogan Ulus (2015).
- Shape Expressions for Specifying and Extracting Signal Features.
  RV paper with Dejan Nickovic, Xin Qin, Cristinel Mateis, and Jyotirmoy Deshmukh (2019). Best paper award.
- Specifying and Detecting Temporal Patterns with Shape Expressions.
  STTT paper with Dejan Nickovic, Xin Qin, Cristinel Mateis, and Jyotirmoy Deshmukh (2021).
Tools
The above monitoring, pattern matching, measurement and diagnostics algorithms are implemented in an academic software tool.
- AMT2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic.
  TACAS tool paper with Dejan Nickovic, Olivier Lebeltel, Oded Maler and Dogan Ulus (2018).
- AMT2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic.
  STTT paper with Dejan Nickovic, Olivier Lebeltel, Oded Maler and Dogan Ulus (2020).