New Algorithmic Approaches to Point Constellation Recognition. - Thomas Bourgeat; Julien Bringer; Hervé Chabanne; Robin Champenois; Jérémie Clément; Houda Ferradi; Marc Heinrich; Paul Melotti; David Naccache; Antoine Voizard (SEC, 2014)

Specification Mining for Asynchronous Controllers. - Javier de San Pedro; Thomas Bourgeat; Jordi Cortadella (ASYNC, 2016)

Composable Building Blocks to Open up Processor Design. - Sizhuo Zhang; Andrew Wright; Thomas Bourgeat; Arvind 001 (MICRO, 2018)

MI6: Secure Enclaves in a Speculative Out-of-Order Processor. - Thomas Bourgeat; Ilia A. Lebedev; Andrew Wright; Sizhuo Zhang; Arvind 001; Srinivas Devadas (MICRO, 2019)

Composable Building Blocks to Open Up Processor Design. - Sizhuo Zhang; Andrew Wright; Thomas Bourgeat (IEEE Micro, 2019)

AQUOMAN: An Analytic-Query Offloading Machine. - Shuotao Xu; Thomas Bourgeat; Tianhao Huang; Hojun Kim; Sungjin Lee 001; Arvind 001 (MICRO, 2020)

The essence of Bluespec: a core language for rule-based hardware design. - Thomas Bourgeat; Clément Pit-Claudel; Adam Chlipala; Arvind 001 (PLDI, 2020)

Robomorphic computing: a design methodology for domain-specific accelerators parameterized by robot morphology. - Sabrina M. Neuman; Brian Plancher; Thomas Bourgeat; Thierry Tambe; Srinivas Devadas; Vijay Janapa Reddi (ASPLOS, 2021)

Effective simulation and debugging for a high-level hardware language using software compilers. - Clément Pit-Claudel; Thomas Bourgeat; Stella Lau; Arvind 001; Adam Chlipala (ASPLOS, 2021)

FlexMiner: A Pattern-Aware Accelerator for Graph Pattern Mining. - Xuhao Chen 001; Tianhao Huang; Shuotao Xu; Thomas Bourgeat; Chanwoo Chung; Arvind 001 (ISCA, 2021)

A Multipurpose Formal RISC-V Specification. - Thomas Bourgeat; Ian Clester; Andres Erbsen; Samuel Gruetter; Andrew Wright; Adam Chlipala (CoRR, 2021)

Accelerating Robot Dynamics Gradients on a CPU, GPU, and FPGA. - Brian Plancher; Sabrina M. Neuman; Thomas Bourgeat; Scott Kuindersma; Srinivas Devadas; Vijay Janapa Reddi (IEEE Robotics Autom. Lett., 2021)

DAGguise: mitigating memory timing side channels. - Peter W. Deutsch; Yuheng Yang; Thomas Bourgeat; Jules Drean; Joel S. Emer; Mengjia Yan 001 (ASPLOS, 2022)

Metior: A Comprehensive Model to Evaluate Obfuscating Side-Channel Defense Schemes. - Peter W. Deutsch; Weon Taek Na; Thomas Bourgeat; Joel S. Emer; Mengjia Yan 001 (ISCA, 2023)

RoboShape: Using Topology Patterns to Scalably and Flexibly Deploy Accelerators Across Robots. - Sabrina M. Neuman; Radhika Ghosal; Thomas Bourgeat; Brian Plancher; Vijay Janapa Reddi (ISCA, 2023)

Pensieve: Microarchitectural Modeling for Security Evaluation. - Yuheng Yang; Thomas Bourgeat; Stella Lau; Mengjia Yan 001 (ISCA, 2023)

Citadel: Side-Channel-Resistant Enclaves with Secure Shared Memory on a Speculative Out-of-Order Processor. - Jules Drean; Miguel Gomez-Garcia; Thomas Bourgeat; Srinivas Devadas (CoRR, 2023)

Specification and verification of sequential machines in rule-based hardware languages - Thomas Bourgeat (2023)

Flexible Instruction-Set Semantics via Abstract Monads (Experience Report). - Thomas Bourgeat; Ian Clester; Andres Erbsen; Samuel Gruetter; Pratap Singh; Andy Wright; Adam Chlipala (Proc. ACM Program. Lang., 2023)

Specification and Verification of Strong Timing Isolation of Hardware Enclaves. - Stella Lau; Thomas Bourgeat; Clément Pit-Claudel; Adam Chlipala (CCS, 2024)

Verifying Software Emulation of an Unsupported Hardware Instruction. - Samuel Gruetter; Thomas Bourgeat; Adam Chlipala (ITP, 2024)

Performance Interfaces for Hardware Accelerators. - Jiacheng Ma 002; Rishabh R. Iyer; Sahand Kashani; Mahyar Emami; Thomas Bourgeat; George Candea (OSDI, 2024)

Formal Verification for Secure Processors: A Guide for Computer Architects. - Mengjia Yan 001; Thomas Bourgeat; Sharad Malik (Computer, 2024)

Parendi: Thousand-Way Parallel RTL Simulation. - Mahyar Emami; Thomas Bourgeat; James R. Larus (ASPLOS (2), 2025)

RTL Verification for Secure Speculation Using Contract Shadow Logic. - Qinhan Tan; Yuheng Yang; Thomas Bourgeat; Sharad Malik; Mengjia Yan 001 (ASPLOS (1), 2025)

Interoperability of Proof Systems with SC-TPTP. - Simon Guilloud; Julie Cailler; Sankalp Gambhir; Auguste Poiroux; Yann Herklotz; Thomas Bourgeat; Viktor Kuncak (CADE, 2025)

Lightweight Hypervisor Verification: Putting the Hardware Burger on a Diet. - Charly Castes; François Costa; Nate Foster; Thomas Bourgeat; Edouard Bugnion (HotOS, 2025)

Making Concurrent Hardware Verification Sequential. - Thomas Bourgeat; Jiazheng Liu; Adam Chlipala; Arvind 001 (PLDI, 2025)

Automatic ISA analysis for Secure Context Switching. - Neelu S. Kalani; Thomas Bourgeat; Guerney D. H. Hunt; Wojciech Ozga (CoRR, 2025)

CaSA: End-to-End Quantitative Security Analysis of Randomly Mapped Caches. - Thomas Bourgeat; Jules Drean; Yuheng Yang; Lillian Tsai; Joel S. Emer; Mengjia Yan 001 (IEEE Des. Test, 2025)

SystolicAttention: Fusing FlashAttention within a Single Systolic Array. - Jiawei Lin; Guokai Chen; Yuanlong Li; Thomas Bourgeat (CoRR, 2025)