VCA: Verification and Computer Architecture

VCA is a lab at EPFL in the School of Computer and Communication Sciences. Our research lies at the intersection of programming languages, formal methods, and computer architecture.

Our primary focus is hardware semantics and formal verification. We develop precise mathematical models of hardware designs—from processors and dataflow circuits to cache coherence protocols—and use interactive theorem provers to prove their correctness. This includes compositional proof techniques for concurrent hardware modules and methods that make hardware verification more scalable and trustworthy.

We also work on interfacing hardware and software through precise specifications. Modern systems rely on clean contracts between layers—ISA specifications, hypervisor interfaces, and firmware boundaries. We ensure that hardware faithfully implements its specifications and that system software can be verified against them, bridging architecture, programming languages, and operating systems research.

Finally, we develop security verification techniques for hardware, applying taint tracking and contract-based reasoning to detect information leakage and speculation vulnerabilities at the RTL level.

We also are working on the design of abstractions that are compatible with the necessities of today’s compute stack, in particular we are developping abstractions for interconnecting accelerators and abstraction for rack-scale computers.

Recent Publications and Preprints

ASPLOS '26a: Yuheng Yang, Qinhan Tan, Thomas Bourgeat, Sharad Malik, and Mengjia Yan. Compass: Navigating the Design Space of Taint Schemes for RTL Security Verification. DOI
ASPLOS '26b: Yann Herklotz, Ayatallah Elakhras, Martina Camaioni, Paolo Ienne, Lana Josipovic, and Thomas Bourgeat. Graphiti: Formally Verified Out-of-Order Execution in Dataflow Circuits. [ DOI | artefact | pdf ]
IEEE RAL '26: Alp Eren Yilmaz, Thomas Bourgeat, Lillian Pentecost, Brian Plancher, and Sabrina M. Neuman. RoboPrec: Enabling Reliable Embedded Computing for Robotics by Providing Accuracy Guarantees Across Mixed-Precision Datatypes. DOI
CPP '26: Martina Camaioni, Yann Herklotz, Tz-Ching Yu, and Thomas Bourgeat. Towards Composable Proofs of Cache Coherence Protocols. [ DOI | artefact | pdf ]
IEEE D&T '25: Thomas Bourgeat, Jules Drean, Yuheng Yang, Lillian Tsai, Joel S. Emer, and Mengjia Yan. CaSA: End-to-End Quantitative Security Analysis of Randomly Mapped Caches. DOI
SOSP '25a: Jiacheng Ma, Jonas Kaufmann, Emilien Guandalino, Rishabh R. Iyer, Thomas Bourgeat, and George Candea. Fast End-to-End Performance Simulation of Accelerated Hardware-Software Stacks. DOI
CADE '25: Simon Guilloud, Julie Cailler, Sankalp Gambhir, Auguste Poiroux, Yann Herklotz, Thomas Bourgeat, and Viktor Kuncak. Interoperability of Proof Systems with SC-TPTP. DOI
HotOS '25: Charly Castes, François Costa, Nate Foster, Thomas Bourgeat, and Edouard Bugnion. Lightweight Hypervisor Verification: Putting the Hardware Burger on a Diet. DOI
PLDI '25: Thomas Bourgeat, Jiazheng Liu, Adam Chlipala, and Arvind. Making Concurrent Hardware Verification Sequential. DOI
ASPLOS '25a: Mahyar Emami, Thomas Bourgeat, and James R. Larus. Parendi: Thousand-Way Parallel RTL Simulation. DOI
ASPLOS '25b: Qinhan Tan, Yuheng Yang, Thomas Bourgeat, Sharad Malik, and Mengjia Yan. RTL Verification for Secure Speculation Using Contract Shadow Logic. DOI
USENIX '25: Neelu S. Kalani, Thomas Bourgeat, Guerney D. H. Hunt, and Wojciech Ozga. Save what must be saved: Secure context switching with Sailor. [ pdf | http ]
SOSP '25b: Charly Castes, François Costa, Neelu S. Kalani, Timothy Roscoe, Nate Foster, Thomas Bourgeat, and Edouard Bugnion. The Design and Implementation of a Virtual Firmware Monitor. DOI
SOSP '25c: Tao Lyu, Kumar Kartikeya Dwivedi, Thomas Bourgeat, Mathias Payer, Meng Xu, and Sanidhya Kashyap. eBPF Misbehavior Detection: Fuzzing with a Specification-Based Oracle. DOI
COMPUTER '24: Mengjia Yan, Thomas Bourgeat, and Sharad Malik. Formal Verification for Secure Processors: A Guide for Computer Architects. DOI
OSDI '24: Jiacheng Ma, Rishabh R. Iyer, Sahand Kashani, Mahyar Emami, Thomas Bourgeat, and George Candea. Performance Interfaces for Hardware Accelerators. http
CCS '24: Stella Lau, Thomas Bourgeat, Clément Pit-Claudel, and Adam Chlipala. Specification and Verification of Strong Timing Isolation of Hardware Enclaves. DOI
ITP '24: Samuel Gruetter, Thomas Bourgeat, and Adam Chlipala. Verifying Software Emulation of an Unsupported Hardware Instruction. DOI
Preprint: Jiawei Lin, Guokai Chen, Yuanlong Li, and Thomas Bourgeat. SystolicAttention: Fusing FlashAttention within a single systolic array, 2025.
[ arXiv | pdf ]