Add initial filesHEADmaster

1 files changed, 509 insertions, 0 deletions

diff --git a/paper/conference.bib b/paper/conference.bib
new file mode 100644
index 0000000..43c8599
--- /dev/null
+++ b/paper/conference.bib
@@ -0,0 +1,509 @@
+@incollection{wang09_chapt_logic,
+  address =      "Boston",
+  author =       "Jie-Hong Jiang and Srinivas Devadas",
+  booktitle =    "Electronic Design Automation",
+  doi =          "10.1016/B978-0-12-374364-0.50013-8",
+  editor =       "Laung-Terng Wang and Yao-Wen Chang and Kwang-Ting Cheng",
+  isbn =         "978-0-12-374364-0",
+  pages =        "299 - 404",
+  publisher =    "Morgan Kaufmann",
+  title =        "CHAPTER 6 - Logic synthesis in a nutshell",
+  year =         2009,
+}
+
+@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},
+  acmid =        1993532,
+  address =      {New York, NY, USA},
+  isbn =         {978-1-4503-0663-8},
+  keywords =     {automated testing, compiler defect, compiler testing, random
+                  program generation, random testing},
+  location =     {San Jose, California, USA},
+  numpages =     12,
+  publisher =    {ACM},
+  series =       {PLDI '11},
+}
+
+@software{herklotz_verismith,
+  author       = {Yann Herklotz and
+                  John Wickerson},
+  title        = {Verismith: FPGA '20 Artifact},
+  month        = dec,
+  year         = 2019,
+  publisher    = {Zenodo},
+  version      = {fpga20},
+  doi          = {10.5281/zenodo.3559802},
+  url          = {https://doi.org/10.5281/zenodo.3559802}
+}
+
+@inproceedings{regehr12_test_reduc_c_compil_bugs,
+  author =       {Regehr, John and Chen, Yang and Cuoq, Pascal and Eide, Eric
+                  and Ellison, Chucky and Yang, Xuejun},
+  title =        {Test-case Reduction for C Compiler Bugs},
+  booktitle =    {Proceedings of the 33rd ACM SIGPLAN Conference on Programming
+                  Language Design and Implementation},
+  year =         2012,
+  pages =        {335--346},
+  doi =          {10.1145/2254064.2254104},
+  url =          {https://doi.org/10.1145/2254064.2254104},
+  acmid =        2254104,
+  address =      {New York, NY, USA},
+  isbn =         {978-1-4503-1205-9},
+  keywords =     {automated testing, bug reporting, compiler defect, compiler
+                  testing, random testing, test-case minimization},
+  location =     {Beijing, China},
+  numpages =     12,
+  publisher =    {ACM},
+  series =       {PLDI '12},
+}
+
+@inproceedings{lidbury15_many_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},
+  url =          {https://doi.org/10.1145/2737924.2737986},
+  acmid =        2737986,
+  address =      {New York, NY, USA},
+  isbn =         {978-1-4503-3468-6},
+  keywords =     {Compilers, GPUs, OpenCL, concurrency, metamor- phic testing,
+                  random testing},
+  location =     {Portland, OR, USA},
+  numpages =     12,
+  publisher =    {ACM},
+  series =       {PLDI '15},
+}
+
+@incollection{seligman15_chapt_formal,
+  address =      "Boston",
+  author =       "Erik Seligman and Tom Schubert and M V Achutha Kiran Kumar",
+  booktitle =    "Formal Verification",
+  doi =          "10.1016/B978-0-12-800727-3.00008-3",
+  editor =       "Erik Seligman and Tom Schubert and M V Achutha Kiran Kumar",
+  isbn =         "978-0-12-800727-3",
+  keywords =     "Formal Equivalence Verification (FEV), Equivalence Checking
+                  (EC), combinational equivalence, sequential equivalence,
+                  optimization, synthesis",
+  pages =        "225 - 259",
+  publisher =    "Morgan Kaufmann",
+  title =        "Chapter 8 - Formal equivalence verification",
+  year =         2015,
+}
+
+@misc{wolf_yosys_open_synth_suite,
+  author =       {Clifford Wolf},
+  title =        {{Yosys Open SYnthesis Suite}},
+  url =          {https://bit.ly/2kAXg0q},
+  urldate =      {2019-01-11},
+  year = 2019,
+}
+
+@misc{joyce_dan_joyces,
+  author =       {Dan Joyce},
+  title =        {Dan Joyce's 16 bug types only found with gate-level
+                  simulation},
+  url =          {https://bit.ly/2nnO22M},
+  urldate =      {2019-08-02},
+  year = 2019,
+}
+
+@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},
+ booktitle = {Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation},
+ series = {PLDI '19},
+ year = {2019},
+ isbn = {978-1-4503-6712-7},
+ location = {Phoenix, AZ, USA},
+ pages = {1041--1053},
+ numpages = {13},
+ doi = {10.1145/3314221.3314622},
+ acmid = {3314622},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ keywords = {compiler verification, hardware verification, program verification, verified stack},
+}
+
+@inproceedings{mcdonald06_logic_equiv_check_arriv_fpga_devel,
+  author =       {McDonald, William and Liao, Janny},
+  title =        {Logic Equivalence Checking has Arrived for {FPGA} Developers},
+  booktitle =    {Design and Verification Conference (DVCon)},
+  year =         2006,
+  month =        Jan,
+}
+
+@techreport{05_veril_regis_trans_level_synth,
+  type =       {Standard},
+  key = {IEEE Std 1364.1},
+  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},
+  ISSN =         {},
+  keywords =     {IEC Standards;Verilog;Registers},
+  month =        {},
+}
+
+@article{mckeeman98_differ_testin_softw,
+  author =       {McKeeman, William M},
+  title =        {Differential Testing for Software},
+  journal =      {Digital Technical Journal},
+  volume =       10,
+  number =       1,
+  pages =        {100--107},
+  year =         1998,
+}
+
+@article{zeller02_simpl_isolat_failur_induc_input,
+  author =       {A. {Zeller} and R. {Hildebrandt}},
+  title =        {Simplifying and Isolating Failure-Inducing Input},
+  journal =      {IEEE Transactions on Software Engineering},
+  volume =       28,
+  number =       2,
+  pages =        {183-200},
+  year =         2002,
+  doi =          {10.1109/32.988498},
+  url =          {https://doi.org/10.1109/32.988498},
+  keywords =     {program debugging;program testing;online front-ends;test
+                  case;delta debugging algorithm;failure-inducing input;Mozilla
+                  web browser;user actions;HTML;500 MHz;Vehicle crash
+                  testing;Debugging;Automatic testing;HTML;Computer
+                  crashes;Computer Society;Prototypes;Databases;Computer
+                  bugs;Turning},
+  month =        {Feb},
+}
+
+@misc{xilinx_vivad_desig_suite,
+  author =       {Xilinx},
+  title =        {{Vivado Design Suite}},
+  url =          {https://bit.ly/2wZAmld},
+  urldate =      {2019-01-14},
+  year = 2019,
+}
+
+@misc{xilinx_xst_synth_overv,
+  author =       {Xilinx},
+  title =        {{XST} Synthesis Overview},
+  url = {https://bit.ly/2lGtkjL},
+  urldate =      {2019-01-11},
+  year = 2019,
+}
+
+@misc{wolf_vlogh,
+  author =       {Clifford Wolf},
+  title =        {{VlogHammer}},
+  url =          {https://bit.ly/2kCxjO3},
+  urldate =      {2019-01-11},
+  year = 2019,
+}
+
+@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},
+  journal =      {Proc. ACM Program. Lang.},
+  volume =       1,
+  number =       {ICFP},
+  pages =        {24:1--24:30},
+  year =         2017,
+  doi =          {10.1145/3110268},
+  acmid =        3110268,
+  address =      {New York, NY, USA},
+  articleno =    24,
+  issn =         {2475-1421},
+  issue_date =   {September 2017},
+  keywords =     {formal verification, hardware, proof assistants},
+  month =        Aug,
+  numpages =     30,
+  publisher =    {ACM},
+}
+
+@misc{intel_intel_quart,
+  author =       {Intel},
+  title =        {{Intel Quartus}},
+  url =
+                  {https://intel.ly/2m7wbCs},
+  urldate =      {2019-01-14},
+  year = 2019,
+}
+
+@misc{cadence_confor_equiv_check,
+  author =       {Cadence},
+  title =        {{Conformal Equivalence Checker}},
+  url =          {https://bit.ly/2mkp0aa},
+  urldate =      {2019-01-14},
+  year = 2019,
+}
+
+@inproceedings{ratchev03_verif_correc_fpga_logic_synth_algor,
+  author =       {Ratchev, Boris and Hutton, Mike and Baeckler, Gregg and van
+                  Antwerpen, Babette},
+  title =        {Verifying the Correctness of FPGA Logic Synthesis Algorithms},
+  booktitle =    {Proceedings of the 2003 ACM/SIGDA Eleventh International
+                  Symposium on Field Programmable Gate Arrays},
+  year =         2003,
+  pages =        {127--135},
+  doi =          {10.1145/611817.611837},
+  url =          {https://doi.org/10.1145/611817.611837},
+  acmid =        611837,
+  address =      {New York, NY, USA},
+  isbn =         {1-58113-651-X},
+  keywords =     {FPGA, programmable logic, synthesis, test, verification},
+  location =     {Monterey, California, USA},
+  numpages =     9,
+  publisher =    {ACM},
+  series =       {FPGA '03},
+}
+
+@inproceedings{aagaard91,
+  author =       {M. {Aagaard} and M. {Leeser}},
+  title =        {A formally verified system for logic synthesis},
+  booktitle =    {[1991 Proceedings] IEEE International Conference on Computer
+                  Design: VLSI in Computers and Processors},
+  year =         1991,
+  pages =        {346-350},
+  doi =          {10.1109/ICCD.1991.139915},
+  keywords =     {Boolean functions;formal specification;logic CAD;formally
+                  verified system;logic synthesis;correctness;weak division
+                  algorithm;Boolean simplification;programming language ML;Nuprl
+                  proof development
+                  system;errors;implementation;Hardware;Algorithm design and
+                  analysis;Registers;Logic programming;Computer
+                  languages;Process design;Boolean algebra;High level
+                  synthesis;Circuit synthesis;Boolean functions},
+  month =        Oct,
+}
+
+@inproceedings{braibant13_formal_verif_hardw_synth,
+  author =       "Braibant, Thomas and Chlipala, Adam",
+  title =        "Formal Verification of Hardware Synthesis",
+  booktitle =    "Computer Aided Verification",
+  year =         2013,
+  pages =        "213--228",
+  abstract =     "We report on the implementation of a certified compiler for a
+                  high-level hardware description language (HDL) called Fe-Si
+                  (FEatherweight SynthesIs). Fe-Si is a simplified version of
+                  Bluespec, an HDL based on a notion of guarded atomic
+                  actions. Fe-Si is defined as a dependently typed deep
+                  embedding in Coq. The target language of the compiler
+                  corresponds to a synthesisable subset of Verilog or VHDL. A
+                  key aspect of our approach is that input programs to the
+                  compiler can be defined and proved correct inside Coq. Then,
+                  we use extraction and a Verilog back-end (written in OCaml) to
+                  get a certified version of a hardware design.",
+  address =      "Berlin, Heidelberg",
+  editor =       "Sharygina, Natasha and Veith, Helmut",
+  isbn =         "978-3-642-39799-8",
+  publisher =    "Springer",
+}
+
+@InProceedings{flor18_pi_ware,
+  author =       {Jo{\~a}o Paulo Pizani Flor and Wouter Swierstra and Yorick
+                  Sijsling},
+  title =        {{Pi-Ware: Hardware Description and Verification in Agda}},
+  booktitle =    {21st International Conference on Types for Proofs and Programs
+                  (TYPES 2015)},
+  year =         2018,
+  volume =       69,
+  pages =        {9:1--9:27},
+  doi =          {10.4230/LIPIcs.TYPES.2015.9},
+  url =          {https://doi.org/10.4230/LIPIcs.TYPES.2015.9},
+  ISBN =         {978-3-95977-030-9},
+  ISSN =         {1868-8969},
+  URN =          {urn:nbn:de:0030-drops-84791},
+  address =      {Dagstuhl, Germany},
+  annote =       {Keywords: dependently typed programming, Agda, EDSL, hardware
+                  description languages, functional programming},
+  editor =       {Tarmo Uustalu},
+  publisher =    {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
+  series =       {Leibniz International Proceedings in Informatics (LIPIcs)},
+}
+
+@misc{constable86_implem_mathem_nuprl_proof_devel_system,
+  author =       {Robert L. Constable and others},
+  title =        {Implementing Mathematics with The Nuprl Proof Development
+                  System},
+  year =         1986,
+}
+
+@misc{mcpeak_delta,
+  author =       {Scott McPeak},
+  title =        {{Delta}},
+  url =          {https://bit.ly/2kncyG5},
+  urldate =      {2019-06-11},
+  year = 2019,
+}
+
+@inproceedings{leroy06_formal_certif_compil_back,
+  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},
+  acmid =        1111042,
+  address =      {New York, NY, USA},
+  isbn =         {1-59593-027-2},
+  keywords =     {certified compilation, compiler transformations and
+                  optimizations, program proof, semantic preservation, the Coq
+                  theorem prover},
+  location =     {Charleston, South Carolina, USA},
+  numpages =     13,
+  publisher =    {ACM},
+  series =       {POPL '06},
+}
+
+@InProceedings{brayton10_abc,
+  author =       "Brayton, Robert and Mishchenko, Alan",
+  title =        {{ABC}: An academic industrial-strength verification tool},
+  booktitle =    "Computer Aided Verification",
+  year =         2010,
+  pages =        "24--40",
+  abstract =     "ABC is a public-domain system for logic synthesis and formal
+                  verification of binary logic circuits appearing in synchronous
+                  hardware designs. ABC combines scalable logic transformations
+                  based on And-Inverter Graphs (AIGs), with a variety of
+                  innovative algorithms. A focus on the synergy of sequential
+                  synthesis and sequential verification leads to improvements in
+                  both domains. This paper introduces ABC, motivates its
+                  development, and illustrates its use in formal verification.",
+  address =      "Berlin, Heidelberg",
+  editor =       "Touili, Tayssir and Cook, Byron and Jackson, Paul",
+  isbn =         "978-3-642-14295-6",
+  publisher =    "Springer",
+}
+
+@InProceedings{moura08_z3,
+  author =       "de Moura, Leonardo and Bj{\o}rner, Nikolaj",
+  title =        {{Z3}: An Efficient {SMT} Solver},
+  booktitle =    "Tools and Algorithms for the Construction and Analysis of
+                  Systems",
+  year =         2008,
+  pages =        "337--340",
+  abstract =     "Satisfiability Modulo Theories (SMT) problem is a decision
+                  problem for logical first order formulas with respect to
+                  combinations of background theories such as: arithmetic,
+                  bit-vectors, arrays, and uninterpreted functions. Z3 is a new
+                  and efficient SMT Solver freely available from Microsoft
+                  Research. It is used in various software verification and
+                  analysis applications.",
+  address =      "Berlin, Heidelberg",
+  editor =       "Ramakrishnan, C. R.  and Rehof, Jakob",
+  isbn =         "978-3-540-78800-3",
+  publisher =    "Springer",
+}
+
+@techreport{barrett17_smt_lib_stand,
+  author =       {Clark Barrett and Pascal Fontaine and Cesare Tinelli},
+  institution =  {Department of Computer Science, The University of Iowa},
+  title =        {{The SMT-LIB Standard: Version 2.6}},
+  year =         2017,
+}
+
+@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)},
+  pages =        {1--560},
+  year =         2006,
+  doi =          {10.1109/IEEESTD.2006.99495},
+}
+
+@misc{zalewski15_americ,
+  author =       {Zalewski, Michal},
+  title =        {American fuzzy lop},
+  url =          {http://lcamtuf.coredump.cx/afl/},
+  urldate =      {2019-01-15},
+  year =         2015,
+}
+
+@inproceedings{misherghi06_hdd,
+  author =       {Misherghi, Ghassan and Su, Zhendong},
+  title =        {HDD: Hierarchical Delta Debugging},
+  booktitle =    {Proceedings of the 28th International Conference on Software
+                  Engineering},
+  year =         2006,
+  pages =        {142--151},
+  doi =          {10.1145/1134285.1134307},
+  url =          {https://doi.org/10.1145/1134285.1134307},
+  acmid =        1134307,
+  address =      {New York, NY, USA},
+  isbn =         {1-59593-375-1},
+  keywords =     {automated debugging, delta debugging},
+  location =     {Shanghai, China},
+  numpages =     10,
+  publisher =    {ACM},
+  series =       {ICSE '06},
+}
+
+@inproceedings{brummayer09_fuzzin_delta_smt_solver,
+  author =       {Brummayer, Robert and Biere, Armin},
+  title =        {Fuzzing and Delta-debugging SMT Solvers},
+  booktitle =    {Proceedings of the 7th International Workshop on
+                  Satisfiability Modulo Theories},
+  year =         2009,
+  pages =        {1--5},
+  doi =          {10.1145/1670412.1670413},
+  url =          {https://doi.org/10.1145/1670412.1670413},
+  acmid =        1670413,
+  address =      {New York, NY, USA},
+  isbn =         {978-1-60558-484-3},
+  location =     {Montreal, Canada},
+  numpages =     5,
+  publisher =    {ACM},
+  series =       {SMT '09},
+}
+
+@inproceedings{tao10_autom_testin_approac_compil_based,
+  author =       {Q. {Tao} and W. {Wu} and C. {Zhao} and W. {Shen}},
+  title =        {An Automatic Testing Approach for Compiler Based on
+                  Metamorphic Testing Technique},
+  booktitle =    {2010 Asia Pacific Software Engineering Conference},
+  year =         2010,
+  pages =        {270-279},
+  doi =          {10.1109/APSEC.2010.39},
+  url =          {https://doi.org/10.1109/APSEC.2010.39},
+  keywords =     {automatic programming;formal verification;program
+                  compilers;program testing;software development
+                  management;automatic testing;metamorphic testing;compiler
+                  testing;equivalence preservation relation;Mettoc;fault
+                  detection capability;Testing;Program
+                  processors;Semantics;Equations;Grammar;Software
+                  systems;compiler;metamorphic testing;test automation;test
+                  oracle;test input generation},
+  month =        {Nov},
+}
+
+@misc{intel_intel_fpga_sdk_openc,
+  author =       {Intel},
+  title =        {{Intel} {FPGA} {SDK} for {OpenCL} software technology},
+  url =          {https://intel.ly/2WXoTj8},
+  urldate =      {2019-11-07},
+  year = 2019,
+}
+
+@misc{williams_icarus_veril,
+  author =       {Stephen Williams},
+  title =        {Icarus Verilog},
+  url =          {http://iverilog.icarus.com/},
+  urldate =      {2019-12-14},
+  year = 2019,
+}