1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
|
@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},
}
|
