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
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
|
@article{lahti19_are_we_there_yet,
author = {S. {Lahti} and P. {Sj{\"o}vall} and J. {Vanne} and T. D. {H{\"a}m{\"a}l{\"a}inen}},
title = {Are We There Yet? a Study on the State of High-Level Synthesis},
journal = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},
volume = {38},
number = {5},
pages = {898-911},
year = {2019},
doi = {10.1109/TCAD.2018.2834439},
url = {https://doi.org/10.1109/TCAD.2018.2834439},
ISSN = {1937-4151},
month = {May}
}
@phdthesis{canis15_legup,
keywords = {high-level synthesis, hardware/software co-simulation, FPGA},
title = {Legup: open-source high-level synthesis research framework},
author = {Canis, Andrew Christopher},
year = {2015}
}
@book{bertot04_inter_theor_provin_progr_devel,
keywords = {coq, verification},
author = {Yves Bertot and Pierre Cast{\'{e}}ran},
title = {Interactive Theorem Proving and Program Development},
year = 2004,
publisher = {Springer Berlin Heidelberg},
url = {https://doi.org/10.1007/978-3-662-07964-5},
doi = {10.1007/978-3-662-07964-5}
}
@phdthesis{coquand86,
title = {The calculus of constructions},
author = {Coquand, Thierry and Huet, G{\'e}rard},
year = {1986},
school = {INRIA}
}
@inproceedings{loow21_lutsig,
author = {L\"{o}\"{o}w, Andreas},
title = {Lutsig: A Verified Verilog Compiler for Verified Circuit Development},
year = {2021},
isbn = {9781450382991},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3437992.3439916},
doi = {10.1145/3437992.3439916},
booktitle = {Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs},
pages = {46–60},
numpages = {15},
location = {Virtual, Denmark},
series = {CPP 2021}
}
@inproceedings{yang11_findin_under_bugs_c_compil,
author = {Yang, Xuejun and Chen, Yang and Eide, Eric and Regehr, John},
title = {Finding and Understanding Bugs in C Compilers},
booktitle = {Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design
and Implementation},
year = 2011,
pages = {283-294},
doi = {10.1145/1993498.1993532},
url = {https://doi.org/10.1145/1993498.1993532},
address = {New York, NY, USA},
isbn = 9781450306638,
location = {San Jose, California, USA},
numpages = 12,
publisher = {Association for Computing Machinery},
series = {PLDI '11}
}
@article{leroy09_formal_verif_realis_compil,
author = {Leroy, Xavier},
title = {Formal Verification of a Realistic Compiler},
tags = {verification},
journal = {Commun. ACM},
volume = 52,
number = 7,
pages = {107--115},
year = 2009,
doi = {10.1145/1538788.1538814},
acmid = 1538814,
address = {New York, NY, USA},
issn = {0001-0782},
issue_date = {July 2009},
month = jul,
numpages = 9,
publisher = {ACM}
}
|
