VCA is a lab at EPFL in the School of Computer and Communication Sciences. Our research lies at the intersection between programming languages and computer architecture.
We are interested in designing high-level hardware programming languages especially to ease hardware verification. We leverage interactive theorem provers to reason about hardware, leading to more scalable and compositional proofs.
We also focus on building novel hardware architectures to support fine-grained and dynamic parallel computations.
We are actively recruiting PhD students and postdocs. If you are a prospective PhD student interested in this kind of research, please apply.
Recent Publications and Preprints
- Preprint
- Jiawei Lin, Guokai Chen, Yuanlong Li, and Thomas Bourgeat.
SystolicAttention: Fusing FlashAttention within a single systolic
array, 2025.
[ arXiv | pdf ] - ASPLOS '26
- Yann Herklotz, Ayatallah Elakhras, Martina Camaioni, Paolo Ienne, Lana
Josipović, and Thomas Bourgeat.
Graphiti: Formally verified out-of-order execution in dataflow
circuits.
In Proceedings of the 31st ACM International Conference on
Architectural Support for Programming Languages and Operating Systems, Volume
2, 2026.
[ DOI | artefact | pdf ] - CPP '26
- Martina Camaioni, Yann Herklotz, Tz-Ching Yu, and Thomas Bourgeat.
Towards composable proofs of cache coherence protocols.
In Proc. of the 15th ACM SIGPLAN Int. Conf. on Certified
Programs and Proofs (CPP), 2026.
[ DOI | artefact | pdf ] - USENIX '25
- Neelu S. Kalani, Thomas Bourgeat, Guerney D. H. Hunt, and Wojciech Ozga.
Save what must be saved: Secure context switching with Sailor.
In Proceedings of the 34th USENIX Security Symposium, 2025.
[ pdf | http ]