Registered user since Wed 12 Jun 2019
My research focuses on formalising the process of converting high-level programming language descriptions to correct hardware that is functionally equivalent to the input. This process is called high-level synthesis (HLS), and allows software to be turned into custom accelerators automatically, which can then be placed on field-programmable gate arrays (FPGAs). An implementation in the Coq theorem prover called Vericert can be found on Github.
|PLDI 2022|| Committee Member in Artifact Evaluation Committee within the Research Artifacts-track|
(OOPSLA 2021) Formal verification of high-level synthesis
|Show activities from other conferences|