Author of the publication

A proof-producing translator for verilog development in HOL.

, and . FormaliSE@ICSE, page 99-108. IEEE / ACM, (2019)

Please choose a person to relate this publication to

To differ between persons with the same name, the academic degree and the title of an important publication will be displayed. You can also use the button next to the name to display some publications already assigned to the person.

 

Other publications of authors with the same name

Matching Plans for Frame Inference in Compositional Reasoning., , , , and . ECOOP, volume 313 of LIPIcs, page 26:1-26:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, (2024)A proof-producing translator for verilog development in HOL., and . FormaliSE@ICSE, page 99-108. IEEE / ACM, (2019)Formal Verification of Correctness and Information Flow Security for an In-Order Pipelined Processor., , , and . FMCAD, page 247-256. IEEE, (2023)Reconciling Verified-Circuit Development and Verilog Development.. FMCAD, page 1-10. IEEE, (2022)Verified compilation on a verified processor., , , , , , and . PLDI, page 1041-1053. ACM, (2019)Exact Separation Logic., , , , , and . CoRR, (2022)Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Extended Version)., , , , , and . CoRR, (2024)A small, but important, concurrency problem in Verilog's semantics? (Work in progress).. MEMOCODE, page 1-6. IEEE, (2022)Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Artifact)., , , , , , and . Dagstuhl Artifacts Ser., 10 (2): 13:1-13:2 (2024)Compositional Symbolic Execution for Correctness and Incorrectness Reasoning., , , , , and . ECOOP, volume 313 of LIPIcs, page 25:1-25:28. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, (2024)