@article{leroy09_formal_verif_realis_compil,
  author =       {Leroy, Xavier},
  title =        {Formal Verification of a Realistic Compiler},
  journal =      {Commun. ACM},
  volume =       52,
  number =       7,
  pages =        {107-115},
  year =         2009,
  doi =          {10.1145/1538788.1538814},
  address =      {New York, NY, USA},
  issn =         {0001-0782},
  issue_date =   {July 2009},
  month =        jul,
  numpages =     9,
  publisher =    {ACM},
}

@inproceedings{lidbury15_many_core_compil_fuzzin,
  author          = {Lidbury, Christopher and Lascu, Andrei and Chong, Nathan and Donaldson,
                  Alastair F.},
  title           = {Many-Core Compiler Fuzzing},
  booktitle       = {Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design
                  and Implementation},
  year            = 2015,
  pages           = {65-76},
  doi             = {10.1145/2737924.2737986},
  address         = {New York, NY, USA},
  isbn            = 9781450334686,
  location        = {Portland, OR, USA},
  numpages        = 12,
  publisher       = {Association for Computing Machinery},
  series          = {PLDI '15},
}

@article{takach16_high_level_synth,
  author          = {A. {Takach}},
  title           = {High-Level Synthesis: Status, Trends, and Future
                  Directions},
  journal         = {IEEE Design Test},
  volume          = {33},
  number          = {3},
  pages           = {116-124},
  year            = {2016},
  doi             = {10.1109/MDAT.2016.2544850},
  url             = {https://doi.org/10.1109/MDAT.2016.2544850},
  ISSN            = {2168-2364},
  month           = {June},
}

@inproceedings{liu16_effic_high_level_synth_desig,
  author          = { {Dong Liu} and B. C. {Schafer}},
  title           = {Efficient and reliable High-Level Synthesis Design Space
                  Explorer for FPGAs},
  booktitle       = {2016 26th International Conference on Field Programmable
                  Logic and Applications (FPL)},
  year            = 2016,
  pages           = {1-8},
  doi             = {10.1109/FPL.2016.7577370},
  ISSN            = {1946-1488},
  month           = {Aug},
}

@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},
  ISSN            = {1937-4151},
  month           = {May},
}

@misc{mentor20_catap_high_level_synth,
  author          = {Mentor},
  title           = {Catapult High-Level Synthesis},
  url             = {https://www.mentor.com/hls-lp/catapult-high-level-synthesis/c-systemc-hls},
  urldate         = {2020-06-06},
  year            = 2020,
}

@inproceedings{gupta03_spark,
  author          = {S. {Gupta} and N. {Dutt} and R. {Gupta} and A. {Nicolau}},
  title           = {{SPARK}: a high-level synthesis framework for applying parallelizing compiler
                  transformations},
  booktitle       = {16th International Conference on VLSI Design, 2003. Proceedings.},
  year            = 2003,
  pages           = {461-466},
  doi             = {10.1109/ICVD.2003.1183177},
  url             = {https://doi.org/10.1109/ICVD.2003.1183177},
  ISSN            = {1063-9667},
  month           = {Jan},
}

@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           = {},
}

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

@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},
  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},
  ISSN =         {1937-4151},
  month =        {July},
}

@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},
  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},
  ISSN = {1937-4151},
  month = {Aug}
}

@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)},
  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},
  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},
  booktitle =    {Proceedings of the 7th International Symposium on Quality
                  Electronic Design},
  year =         2006,
  pages =        {71--78},
  doi =          {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},
}

@inproceedings{leroy06_formal_certif_compil_back_end,
  author = {Leroy, Xavier},
  title = {Formal Certification of a Compiler Back-End or: Programming
                  a Compiler with a Proof Assistant},
  booktitle = {Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium
                  on Principles of Programming Languages},
  year = 2006,
  pages = {42-54},
  doi = {10.1145/1111037.1111042},
  url = {https://doi.org/10.1145/1111037.1111042},
  address = {New York, NY, USA},
  isbn = 1595930272,
  location = {Charleston, South Carolina, USA},
  numpages = 13,
  publisher = {Association for Computing Machinery},
  series = {POPL '06}
}

@book{bertot04_inter_theor_provin_progr_devel,
  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},
}

@inproceedings{tristan08_formal_verif_trans_valid,
  author = {Tristan, Jean-Baptiste and Leroy, Xavier},
  title = {Formal Verification of Translation Validators: A Case Study on
                  Instruction Scheduling Optimizations},
  booktitle = {Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on
                  Principles of Programming Languages},
  year = 2008,
  pages = {17-27},
  doi = {10.1145/1328438.1328444},
  address = {New York, NY, USA},
  isbn = 9781595936899,
  location = {San Francisco, California, USA},
  numpages = 11,
  publisher = {Association for Computing Machinery},
  series = {POPL '08}
}

@inproceedings{kundu08_valid_high_level_synth,
  author          = "Kundu, Sudipta and Lerner, Sorin and Gupta, Rajesh",
  title           = "Validating High-Level Synthesis",
  booktitle       = "Computer Aided Verification",
  year            = 2008,
  pages           = "459--472",
  address         = "Berlin, Heidelberg",
  editor          = "Gupta, Aarti and Malik, Sharad",
  isbn            = "978-3-540-70545-1",
  publisher       = "Springer",
}

@inproceedings{chapman92_verif_bedroc,
  author          = {R. {Chapman} and G. {Brown} and M. {Leeser}},
  title           = {Verified high-level synthesis in BEDROC},
  booktitle       = {[1992] Proceedings The European Conference on Design Automation},
  year            = 1992,
  pages           = {59--63},
  doi             = {10.1109/EDAC.1992.205894},
  month           = {March},
  publisher       = {IEEE Computer Society},
}

@article{hwang91_formal_approac_to_sched_probl,
  author = {C. -. {Hwang} and J. -. {Lee} and Y. -. {Hsu}},
  title = {A Formal Approach To the Scheduling Problem in High Level
                  Synthesis},
  journal = {IEEE Transactions on Computer-Aided Design of Integrated
                  Circuits and Systems},
  volume = 10,
  number = 4,
  pages = {464-475},
  year = 1991,
  doi = {10.1109/43.75629},
  url = {https://doi.org/10.1109/43.75629},
  month = {April}
}

@inproceedings{page91_compil_occam,
  author = {Page, Ian and Luk, Wayne},
  title = {Compiling Occam into field-programmable gate arrays},
  booktitle = {FPGAs, Oxford Workshop on Field Programmable Logic and
                  Applications},
  year = 1991,
  volume = 15,
  pages = {271--283},
}

@inproceedings{grass94_high,
  author = {W. {Grass} and M. {Mutz} and W. -. {Tiedemann}},
  title = {High level synthesis based on formal methods},
  booktitle = {Proceedings of Twentieth Euromicro Conference. System
                  Architecture and Integration},
  year = 1994,
  pages = {83-91},
  doi = {10.1109/EURMIC.1994.390403},
  month = {Sep.}
}

@inproceedings{jifeng93_towar,
  author = "Jifeng, He and Page, Ian and Bowen, Jonathan",
  title = "Towards a provably correct hardware implementation of occam",
  booktitle = "Correct Hardware Design and Verification Methods",
  year = 1993,
  pages = "214--225",
  address = "Berlin, Heidelberg",
  editor = "Milne, George J.  and Pierre, Laurence",
  isbn = "978-3-540-70655-7",
  publisher = "Springer"
}

@article{perna12_mechan_wire_wise_verif_handel_c_synth,
  author = "Juan Perna and Jim Woodcock",
  title = {Mechanised Wire-Wise Verification of {Handel-C} Synthesis},
  journal = "Science of Computer Programming",
  volume = 77,
  number = 4,
  pages = "424 - 443",
  year = 2012,
  doi = "10.1016/j.scico.2010.02.007",
  issn = "0167-6423",
}

@article{perna11_correc_hardw_synth,
  author = "Perna, Juan and Woodcock, Jim and Sampaio, Augusto and Iyoda,
                  Juliano",
  title = {Correct Hardware Synthesis},
  journal = "Acta Informatica",
  volume = 48,
  number = 7,
  pages = "363--396",
  year = 2011,
  doi = "10.1007/s00236-011-0142-y",
  day = 01,
  issn = "1432-0525",
  month = "Dec"
}

@phdthesis{ellis08,
  author = {Ellis, Martin},
  title = {Correct synthesis and integration of compiler-generated function units},
  school = {Newcastle University},
  url = {https://theses.ncl.ac.uk/jspui/handle/10443/828},
  year = {2008},
}

@inproceedings{loow19_verif_compil_verif_proces,
  author =       {L\"{o}\"{o}w, Andreas and Kumar, Ramana and Tan, Yong Kiam and
                  Myreen, Magnus O. and Norrish, Michael and Abrahamsson, Oskar
                  and Fox, Anthony},
  title =        {Verified Compilation on a Verified Processor},
  tags =         {verification},
  booktitle =    {Proceedings of the 40th ACM SIGPLAN Conference on Programming
                  Language Design and Implementation},
  year =         2019,
  pages =        {1041--1053},
  doi =          {10.1145/3314221.3314622},
  acmid =        3314622,
  address =      {New York, NY, USA},
  isbn =         {978-1-4503-6712-7},
  keywords =     {compiler verification, hardware verification, program
                  verification, verified stack},
  location =     {Phoenix, AZ, USA},
  numpages =     13,
  publisher =    {ACM},
  series =       {PLDI 2019},
}

@inproceedings{canis+11,
  author    = {Andrew Canis and
               Jongsok Choi and
               Mark Aldham and
               Victor Zhang and
               Ahmed Kammoona and
               Jason Helge Anderson and
               Stephen Dean Brown and
               Tomasz S. Czajkowski},
  title     = {{LegUp}: high-level synthesis for {FPGA}-based processor/accelerator systems},
  booktitle = {{FPGA}},
  pages     = {33--36},
  publisher = {{ACM}},
  year      = {2011}
}

@inproceedings{choi+18,
  author    = {Young{-}kyu Choi and
               Jason Cong},
  title     = {{HLS}-based optimization and design space exploration for applications
               with variable loop bounds},
  booktitle = {{ICCAD}},
  publisher = {{ACM}},
  year      = {2018}
}

@book{micheli94_synth_optim_digit_circuit,
  author          = {De Micheli, Giovanni},
  title           = {Synthesis and Optimization of Digital Circuits},
  year            = 1994,
  publisher       = {McGraw-Hill Higher Education},
  abstract        = {From the Publisher:Synthesis and Optimization of Digital Circuits offers a
                  modern, up-to-date look at computer-aided design (CAD) of very large-scale
                  integration (VLSI) circuits. In particular, this book covers techniques for
                  synthesis and optimization of digital circuits at the architectural and logic
                  levels, i.e., the generation of performance-and/or area-optimal circuits
                  representations from models in hardware description languages. The book provides a
                  thorough explanation of synthesis and optimization algorithms accompanied by a
                  sound mathematical formulation and a unified notation. The text covers the
                  following topics: modern hardware description languages (e.g., VHDL, Verilog);
                  architectural-level synthesis of data flow and control units, including algorithms
                  for scheduling and resource binding; combinational logic optimization algorithms
                  for two-level and multiple-level circuits; sequential logic optimization methods;
                  and library binding techniques, including those applicable to FPGAs.},
  edition         = {1st},
  isbn            = 0070163332,
}

@article{05_ieee_stand_veril_regis_trans_level_synth,
  title           = {{IEEE} Standard for {Verilog} Register Transfer Level Synthesis},
  journal         = {IEC 62142-2005 First edition 2005-06 IEEE Std 1364.1},
  volume          = {},
  number          = {},
  pages           = {1-116},
  year            = {2005},
  doi             = {10.1109/IEEESTD.2005.339572},
  url             = {https://doi.org/10.1109/IEEESTD.2005.339572},
  ISSN            = {},
  key             = {IEEE Std 1364.1},
  keywords        = {IEC Standards;Verilog;Registers},
  month           = {},
  type            = {Standard},
}

@article{06_ieee_stand_veril_hardw_descr_languag,
  author          = {},
  title           = {{IEEE} Standard for Verilog Hardware Description Language},
  journal         = {IEEE Std 1364-2005 (Revision of IEEE Std 1364-2001)},
  volume          = {},
  number          = {},
  pages           = {1-590},
  year            = {2006},
  doi             = {10.1109/IEEESTD.2006.99495},
  url             = {https://doi.org/10.1109/IEEESTD.2006.99495},
  ISSN            = {},
  key             = {IEEE Std 1364},
  month           = {April},
  type            = {Standard},
}