path: root/references.bib

@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}
}

@inproceedings{kim04_autom_fsmd,
	author = { {Youngsik Kim} and S. {Kopuri} and N. {Mansouri}},
	title = {Automated formal verification of scheduling process using finite state machines with datapath (FSMD)},
	tags = {hls, verification},
	booktitle = {International Symposium on Signals, Circuits and Systems. Proceedings, SCS 2003. (Cat. No.03EX720)},
	year = 2004,
	pages = {110-115},
	doi = {10.1109/ISQED.2004.1283659},
	url = {https://doi.org/10.1109/ISQED.2004.1283659},
	ISSN = {null},
	month = {March}
}

@inproceedings{karfa06_formal_verif_method_sched_high_synth,
	author = {Karfa, C and Mandal, C and Sarkar, D and Pentakota, S R. and
                  Reade, Chris},
	title = {A Formal Verification Method of Scheduling in High-level Synthesis},
	tags = {hls},
	booktitle = {Proceedings of the 7th International Symposium on Quality Electronic Design},
	year = 2006,
	pages = {71--78},
	doi = {10.1109/ISQED.2006.10},
	url = {https://doi.org/10.1109/ISQED.2006.10},
	acmid = 1126731,
	address = {Washington, DC, USA},
	isbn = {0-7695-2523-7},
	numpages = 8,
	publisher = {IEEE Computer Society},
	series = {ISQED '06}
}

@article{chouksey20_verif_sched_condit_behav_high_level_synth,
	author = {R. {Chouksey} and C. {Karfa}},
	title = {Verification of Scheduling of Conditional Behaviors in High-Level Synthesis},
	journal = {IEEE Transactions on Very Large Scale Integration (VLSI) Systems},
	volume = {},
	number = {},
	pages = {1-14},
	year = {2020},
	doi = {10.1109/TVLSI.2020.2978242},
	url = {https://doi.org/10.1109/TVLSI.2020.2978242},
	ISSN = {1557-9999},
	month = {}
}

@article{banerjee14_verif_code_motion_techn_using_value_propag,
	author = {K. {Banerjee} and C. {Karfa} and D. {Sarkar} and C. {Mandal}},
	title = {Verification of Code Motion Techniques Using Value Propagation},
	tags = {hls, verification},
	journal = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},
	volume = 33,
	number = 8,
	pages = {1180-1193},
	year = 2014,
	doi = {10.1109/TCAD.2014.2314392},
	url = {https://doi.org/10.1109/TCAD.2014.2314392},
	ISSN = {1937-4151},
	keywords = {translation validation, compiler optimisation, verification, high-level synthesis},
	month = {Aug}
}

@article{chouksey19_trans_valid_code_motion_trans_invol_loops,
	author = {R. {Chouksey} and C. {Karfa} and P. {Bhaduri}},
	title = {Translation Validation of Code Motion Transformations Involving Loops},
	tags = {hls, verification},
	journal = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},
	volume = 38,
	number = 7,
	pages = {1378-1382},
	year = 2019,
	doi = {10.1109/TCAD.2018.2846654},
	url = {https://doi.org/10.1109/TCAD.2018.2846654},
	ISSN = {1937-4151},
	keywords = {translation validation, verification, compiler optimisation, high-level synthesis},
	month = {July}
}

@inproceedings{pnueli98_trans,
	author = "Pnueli, A.  and Siegel, M.  and Singerman, E.",
	title = "Translation validation",
	booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",
	year = 1998,
	pages = "151--166",
	address = "Berlin, Heidelberg",
	editor = "Steffen, Bernhard",
	isbn = "978-3-540-69753-4",
	publisher = "Springer Berlin Heidelberg"
}

@unpublished{herklotz21_formal_verif_high_level_synth,
	author = {Herklotz, Yann and Pollard, James D. and Ramanathan, Nadesh and Wickerson, John},
	title = {Formal Verification of High-Level Synthesis},
	year = 2021,
	url = {https://yannherklotz.com/docs/drafts/formal_hls.pdf},
	note = {(under review)}
}

@inproceedings{du21_fuzzin_high_level_synth_tools,
  author          = {Herklotz, Yann and Du, Zewei and Ramanathan, Nadesh and Wickerson, John},
  note            = {(to appear)},
  year            = 2021,
  url             = {https://yannherklotz.com/docs/drafts/fuzzing_hls.pdf},
  title           = {An Empirical Study of the Reliability of High-Level Synthesis Tools},
  booktitle       = {29th IEEE International Symposium on Field-Programmable Custom Computing Machines},
}

@misc{polybench,
	author = {Pouchet, Louis-No\"el},
	title = {PolyBench/C: the Polyhedral Benchmark suite},
	url = {http://web.cse.ohio-state.edu/~pouchet.2/software/polybench/},
	year = {2020},
}

@inproceedings{cong06_sdc,
	author = {J. {Cong} and {Zhiru Zhang}},
	title = {An efficient and versatile scheduling algorithm based on SDC formulation},
	booktitle = {43rd ACM/IEEE Design Automation Conference},
	year = 2006,
	pages = {433-438},
	doi = {10.1145/1146909.1147025},
	url = {https://doi.org/10.1145/1146909.1147025},
	ISSN = {0738-100X},
	month = {July}
}

@inproceedings{loow19_proof_trans_veril_devel_hol,
	author = {L\"{o}\"{o}w, Andreas and Myreen, Magnus O.},
	title = {A Proof-producing Translator for Verilog Development in HOL},
	tags = {hls, semantics},
	booktitle = {Proceedings of the 7th International Workshop on Formal Methods in Software Engineering},
	year = 2019,
	pages = {99--108},
	doi = {10.1109/FormaliSE.2019.00020},
	url = {https://doi.org/10.1109/FormaliSE.2019.00020},
	acmid = 3338828,
	address = {Piscataway, NJ, USA},
	location = {Montreal, Quebec, Canada},
	numpages = 10,
	publisher = {IEEE Press},
	series = {FormaliSE '19}
}

@inproceedings{canis11_legup,
	author = {Canis, Andrew and Choi, Jongsok and Aldham, Mark and Zhang, Victor and Kammoona, Ahmed and Anderson, Jason H. and Brown, Stephen and Czajkowski, Tomasz},
	title = {LegUp: High-Level Synthesis for FPGA-Based Processor/Accelerator Systems},
	year = {2011},
	isbn = {9781450305549},
	publisher = {Association for Computing Machinery},
	address = {New York, NY, USA},
	url = {https://doi.org/10.1145/1950413.1950423},
	doi = {10.1145/1950413.1950423},
	booktitle = {Proceedings of the 19th ACM/SIGDA International Symposium on Field Programmable Gate Arrays},
	pages = {33–36},
	numpages = {4},
	location = {Monterey, CA, USA},
	series = {FPGA '11}
}

@inproceedings{bourgeat20_essen_blues,
	author = {Bourgeat, Thomas and Pit-Claudel, Cl\'{e}ment and Chlipala, Adam and Arvind},
	title = {The Essence of Bluespec: A Core Language for Rule-Based Hardware Design},
	booktitle = {Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation},
	year = 2020,
	pages = {243-257},
	doi = {10.1145/3385412.3385965},
	url = {https://doi.org/10.1145/3385412.3385965},
	address = {New York, NY, USA},
	isbn = 9781450376136,
	location = {London, UK},
	numpages = 15,
	publisher = {Association for Computing Machinery},
	series = {PLDI 2020}
}

@article{choi17_kami,
	author = {Choi, Joonwon and Vijayaraghavan, Muralidaran and Sherman, Benjamin and Chlipala, Adam and Arvind},
	title = {Kami: a Platform for High-Level Parametric Hardware Specification and Its Modular Verification},
	tags = {verification},
	journal = {Proc. ACM Program. Lang.},
	volume = 1,
	number = {ICFP},
	pages = {24:1--24:30},
	year = 2017,
	doi = {10.1145/3110268},
	url = {https://doi.org/10.1145/3110268},
	acmid = 3110268,
	address = {New York, NY, USA},
	articleno = 24,
	issn = {2475-1421},
	issue_date = {September 2017},
	month = aug,
	numpages = 30,
	publisher = {ACM}
}

@misc{singh_silver_oak,
title = {{Silver Oak}},
author = {Satnam Singh},
url = {https://github.com/project-oak/silveroak},
}

@article{blazy09_mechan_seman_cligh_subset_c_languag,
	author = "Blazy, Sandrine and Leroy, Xavier",
	title = {Mechanized Semantics for the Clight Subset of the C Language},
	journal = "Journal of Automated Reasoning",
	volume = 43,
	number = 3,
	pages = "263--288",
	year = 2009,
	doi = "10.1007/s10817-009-9148-3",
	url = {https://doi.org/10.1007/s10817-009-9148-3},
	day = 01,
	issn = "1573-0670",
	month = "Oct"
}

@inproceedings{nigam20_predic_accel_desig_time_sensit_affin_types,
  author          = {Nigam, Rachit and Atapattu, Sachille and Thomas, Samuel and Li, Zhijing and
                  Bauer, Theodore and Ye, Yuwei and Koti, Apurva and Sampson, Adrian and Zhang,
                  Zhiru},
  title           = {Predictable Accelerator Design with Time-Sensitive Affine Types},
  booktitle       = {Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design
                  and Implementation},
  year            = 2020,
  pages           = {393-407},
  doi             = {10.1145/3385412.3385974},
  url             = {https://doi.org/10.1145/3385412.3385974},
  address         = {New York, NY, USA},
  isbn            = 9781450376136,
  keywords        = {Affine Type Systems, High-Level Synthesis},
  location        = {London, UK},
  numpages        = 15,
  publisher       = {Association for Computing Machinery},
  series          = {PLDI 2020},
}

@inproceedings{gajski10_what_hls,
	author = {Gajski, Dan and Austin, Todd and Svoboda, Steve},
	booktitle = {Design Automation Conference},
	title = {What input-language is the best choice for high level synthesis (HLS)?},
	year = {2010},
	volume = {},
	number = {},
	pages = {857-858},
	doi = {10.1145/1837274.1837489}
}

@InProceedings{appel11_verif_softw_toolc,
	author = "Appel, Andrew W.",
	editor = "Barthe, Gilles",
	title = "Verified Software Toolchain",
	booktitle = "Programming Languages and Systems",
	year = "2011",
	publisher = "Springer Berlin Heidelberg",
	address = "Berlin, Heidelberg",
	pages = "1--17",
	abstract = "The software toolchain includes static analyzers to check assertions about programs; optimizing compilers to translate programs to machine language; operating systems and libraries to supply context for programs. Our Verified Software Toolchain verifies with machine-checked proofs that the assertions claimed at the top of the toolchain really hold in the machine-language program, running in the operating-system context, on a weakly-consistent-shared-memory machine.",
	isbn = "978-3-642-19718-5"
}

@article{barthe20_formal_c,
	doi = {10.1145/3371075},
	url = {https://doi.org/10.1145/3371075},
	year = {2020},
	month = jan,
	publisher = {Association for Computing Machinery ({ACM})},
	volume = {4},
	number = {{POPL}},
	pages = {1--30},
	author = {Gilles Barthe and Sandrine Blazy and Benjamin Gr{\'{e}}goire and R{\'{e}}mi Hutin and Vincent Laporte and David Pichardie and Alix Trieu},
	title = {Formal verification of a constant-time preserving C compiler},
	journal = {Proceedings of the {ACM} on Programming Languages}
}