path: root/paper/conference.bib

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