Stanford High Assurance Computer Architectures Lab
Principal Investigator
Image of Caroline Trippel Caroline Trippel
Assistant Professor
Advisees
Image of Mohammad Fadiheh Mohammad Fadiheh
Postdoctoral Scholar
Image of Samantha Archer Samantha Archer
PhD Student
Image of Rachel Cleaveland Rachel Cleaveland
PhD Student
Image of Saranyu Chattopadhyay Saranyu Chattopadhyay
PhD Student
Image of Yao Hsiao Yao Hsiao
PhD Student
Image of Daniel Mendoza Daniel Mendoza
PhD Student
Image of Nicholas Mosier Nicholas Mosier
PhD Student
Image of Ioanna Vavelidou Ioanna Vavelidou
PhD Student
Image of Shruti Verma Shruti Verma
Masters Student
Image of Fabio Ibanez Fabio Ibanez
Undergraduate Student
Image of Xiaofu (Kaia) Li Xiaofu (Kaia) Li
Undergraduate Student
Rotation Students (Autumn 2024)
Image of Sally Wang Sally Wang
PhD Student
Image of Nathan Sobotka Nathan Sobotka
PhD Student





Scalable Assurance via Verifiable Hardware-Software Contract

This direction includes projects related to hardware verification. We are seeking to develop automated and scalable verification tool and methodology to enable efficient and effective verification of system-level properties such as correctness of memory consistency model implementation and security guarantees. One example is rtl2uspec that enables verification of hardware memory consistency model for an input hardware design.
Generating Formal Specifications from Natural Language

A rigorous formalization of hardware design requirements is invaluable for verification. However, writing formal specifications is an error-prone and time-consuming manual task, and thus frequently limits the application of verification techniques in practice. We are developing new frameworks (e.g., nl2spec) to translate natural language to formal specifications through integrating LLMs and automated reasoning in order to systemically minimize the overall manual effort required to produce accurate formal specifications.

Featured Publications

In the Media
February, 2018. CheckMate's synthesis of new variants of Meltdown and Spectre:
April, 2017. TriCheck and deficiences in the RISC-V ISA MCM Specification:
March, 2016. STARNet Center for Future Architectures Research (CFAR):

Joining the Lab
We are looking for motivated graduate and undergraduate researchers. If you are interested in joining the lab, please send an email to trippel @ stanford . edu with your resume and CV.