@inproceedings{CPP '23,
author = {Herklotz, Yann and Demange, Delphine and Blazy, Sandrine},
title = {Mechanised Semantics for Gated Static Single Assignment},
year = {2023},
isbn = {9781450391825},
doi = {10.1145/3573105.3575681},
booktitle = {Proc. of the 12th ACM SIGPLAN Int. Conf. on Certified Programs and Proofs (CPP)},
numpages = {15},
keywords = {Verified Compilation, SSA, Gated SSA},
location = {Boston, MA, USA},
url_artefact = {https://zenodo.org/record/7430387},
url_manuscript = {/papers/cpp23_msgssa.pdf},
url_slides = {/docs/cpp23/slides_msgssa.pdf}
}

@inproceedings{FCCM '22,
  author = {Pardalos, Michalis and Herklotz, Yann and Wickerson, John},
  title = {Resource Sharing for Verified High-Level Synthesis},
  year = {2022},
  booktitle = {30th {IEEE} Annual Int. Symp. on Field-Programmable Custom Computing Machines (FCCM)},
  numpages = 5,
  doi = {10.1109/FCCM53951.2022.9786208},
  note = {Short paper, HIPEAC 2022 Paper Award},
  url_manuscript = {/papers/fccm22_rsvhls.pdf},
  url_artefact = {https://github.com/mpardalos/Vericert-Fun}
}

@article{OOPSLA '21,
  author = {Herklotz, Yann and Pollard, James D. and Ramanathan, Nadesh and Wickerson, John},
  title = {Formal Verification of High-Level Synthesis},
  year = {2021},
  number = {OOPSLA},
  numpages = {30},
  journal = {Proc. of the ACM on Programming Languages},
  publisher = {ACM},
  doi = {10.1145/3485494},
  url_manuscript = {/papers/oopsla21_fvhls.pdf},
  url_slides = {/docs/oopsla21/slides_fvhls.pdf},
  url_artefact = {https://github.com/ymherklotz/vericert},
  url_video = {https://youtu.be/clPiKbKVlUA},
  url_poster = {/docs/oopsla21/poster_fvhls.pdf},
  url_changelog = {/changelog/oopsla21_fvhls},
  url_blog_post = {https://vericert.ymhg.org/2021/10/a-first-look-at-vericert/}
}

@inproceedings{FCCM '21,
  author = {Herklotz, Yann and Du, Zewei and Ramanathan, Nadesh and Wickerson, John},
  title = {An Empirical Study of the Reliability of High-Level Synthesis Tools},
  year = {2021},
  booktitle = {29th {IEEE} Annual Int. Symp. on Field-Programmable Custom Computing Machines (FCCM)},
  keywords = {automated testing, compiler defect, compiler testing, random program generation, random testing},
  numpages = 5,
  note = {Short paper},
  doi = {10.1109/FCCM51124.2021.00034},
  url_manuscript = {/papers/fccm21_esrhls.pdf},
  url_artefact = {https://github.com/ymherklotz/fuzzing-hls},
}

@inproceedings{FPGA '20,
  author = {Yann Herklotz and John Wickerson},
  title = {Finding and Understanding Bugs in {FPGA} Synthesis Tools},
  year = 2020,
  booktitle = {ACM/SIGDA Int. Symp. on Field-Programmable Gate Arrays (FPGA)},
  doi = {10.1145/3373087.3375310},
  isbn = {978-1-4503-7099-8/20/02},
  keywords = {automated testing, compiler defect, compiler testing, random program generation, random testing},
  location = {Seaside, CA, USA},
  numpages = 11,
  url_poster = {/docs/msrphd2019/verismith_poster.pdf},
  url_slides = {/docs/fpga2020/verismith_slides.pdf},
  url_blog_post = {/blog/2019-06-19-verismith.html},
  url_manuscript = {/papers/fpga20_fubfst.pdf},
  url_artefact = {https://github.com/ymherklotz/verismith},
}