Professional homepage of Thomas Ferrère
Principal Hardware Engineer, Imagination Technologies.
Research
- Datapath Design
- Computer Arithmetic
- Assertion-Based Verification
- Analog Mixed-Signal Simulation
About me
I am a principal hardware engineer at Imagination Technologies, Kings Langley, UK where I lead the datapath design group as part of the PowerVR hardware graphics division.
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 Siemens EDA.
News
Open positions at Imagination Technologies!
Highlighted Events
Symposium on Computer Arithmetic ARITH,
Symopsium on Microarchitecture MICRO,
Asilomar Conference on Signals, Systems, and Computers ASILOMAR,
Design Automation Conference DAC,
Design Automation and Test in Europe Conference DATE,
Formal Methods in Computer-Aided Design FMCAD,
Design and Verification Conference and Exhibition DVCON,
Symposium on Logic in Computer Science LICS,
Conference on Computer-Aided Verification CAV,
Symposium on Formal Methods FM,
Joint Conferences On Theory and Practice of Software ETAPS,
Runtime Verification RV,
Conference on Embedded Software EMSOFT.
Organisation
PhD Thesis
Assertions and Measurements for Mixed-Signal Simulation, University of Grenoble, 2016.
Patents
- Method and system for calculating dot products GB2615773A (2022).
- Method and system for verifying a sorter US11783105B2 (2021) with Simon Gaulter, Faizan Nazar and Sam Elliott.
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.
- 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.
- 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.
- 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.
- 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.
- 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.
- Tools
The above monitoring, pattern matching, measurement and diagnostics algorithms are implemented in an academic software tool.