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.
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.