@inproceedings(bd:pipeline,
 author       = "J. R. Burch and D. L. Dill",
 year         = "1994",
 title        = "{Automatic Verification of Pipelined Microprocessor Control}",
 editor       = "D. L. Dill",
 booktitle    = "{Proceedings of the $6$th International Conference on Computer-Aided Verification (CAV 1994)}",
 series       = "{LNCS}",
 volume       = "818",
 publisher    = "{Springer-Verlag}",
 pages        = "68--80",
 doi          = "10.1007/3-540-58179-0\_44",
)
@inproceedings(xpilot,
 author       = "J. Cong and Y. Fan and G. Han and W. Jiang and Z. Zhang",
 year         = "2006",
 title        = "Platform-Based Behavior-Level and System-Level Synthesis",
 booktitle    = "2006 IEEE International SoC Conference",
 publisher    = "IEEE",
 pages        = "199--202",
 doi          = "10.1109/SOCC.2006.283880",
)
@book(spark,
 author       = "D. Gajski and N. D. Dutt and A. Wu and S. Lin",
 year         = "1993",
 title        = "{High Level Synthesis: Introduction to Chip and System Design}",
 publisher    = "Kluwer Academic Publishers",
)
@inproceedings(hrx:dac-12,
 author       = "K. Hao and S. Ray and F. Xie",
 year         = "2012",
 title        = "{Equivalence Checking for Behaviorally Synthesized Pipelines}",
 editor       = "P. Groeneveld and D. Sciuto and S. Hassoun",
 booktitle    = "{$49$th International ACM/EDAC/IEEE Design Automation Conference (DAC 2012)}",
 publisher    = "ACM",
 pages        = "344--349",
 doi          = "10.1145/2228360.2228423",
)
@inproceedings(hxry:date-10,
 author       = "K. Hao and F. Xie and S. Ray and J. Yang",
 year         = "2010",
 title        = "Optimizing Equivalence Checking for Behavioral Synthesis",
 booktitle    = "{Design, Automation and Test in Europe (DATE 2010)}",
 publisher    = "{IEEE}",
 pages        = "1500--1505",
)
@misc(Moussa99,
 author       = "{I. Moussa and Z. Sugar and R. Suescun and A. A. Jerraya and M. Diaz-Nava and M. Pavesi and S. Crudo and L. Gazzi}",
 year         = "{1999}",
 title        = "{Comparing RTL and Behavioral Design Methodologies in the Case of a 2M Transistors ATM Shaper}",
 doi          = "10.1145/309847.310006",
)
@book(car,
 author       = "M. Kaufmann and P. Manolios and J S. Moore",
 year         = "2000",
 title        = "Computer-Aided Reasoning: An Approach",
 publisher    = "Kluwer Academic Publishers",
 address      = "{Boston, MA}",
 doi          = "10.1007/978-1-4757-3188-0",
)
@inproceedings(llvm,
 author       = "C. Lattner and V. Adve",
 year         = "2004",
 title        = "{LLVM: A Compilation Framework for Lifelong Program Analysis \& Transformation}",
 booktitle    = "{Proceedings of the 2004 International Symposium on Code Generation and Optimization (CGO 2004)}",
 pages        = "75--84",
 doi          = "10.1109/CGO.2004.1281665",
)
@inproceedings(pm:pipelines,
 author       = "P. Manolios",
 year         = "2000",
 title        = "{Correctness of Pipelined Machines}",
 editor       = "W. A. Hunt, Jr. and S. D. Johnson",
 booktitle    = "{Proceedings of the $3$rd International Conference on Formal Methods in Computer-Aided Design (FMCAD 2000)}",
 series       = "LNCS",
 volume       = "1954",
 publisher    = "{Springer-Verlag}",
 address      = "Austin, TX",
 pages        = "161--178",
 doi          = "10.1007/3-540-40922-X\_11",
)
@inproceedings(moore-fmcad-tutorial,
 author       = "J S. Moore",
 year         = "2011",
 title        = "{The Role of Human Creativity in Mechanized Verification}",
 editor       = "P. Bjesse and A. {Slobodov\'{a}}",
 booktitle    = "{Proceedings of the $11$th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2011)}",
 pages        = "18",
)
@inproceedings(disha-itp14,
 author       = "D. Puri and S. Ray and K. Hao and F. Xie",
 year         = "2014",
 title        = "Mechanical Certification of Loop Pipelining Transformations: A Preview",
 editor       = "G. Klein and R. Gamboa",
 booktitle    = "$4$th International Conference on Interactive Theorem Proving (ITP 2014)",
 series       = "LNCS",
 volume       = "7998",
 publisher    = "Springer",
)
@inproceedings(rhcxy:atva-09,
 author       = "S. Ray and K. Hao and F. Xie and J. Yang",
 year         = "2009",
 title        = "{Formal Verification for High-Assurance Behavioral Synthesis}",
 editor       = "Z. Liu and A. P. Ravn",
 booktitle    = "{Proceedings of the 7th International Symposium on Automated Technology for Verification and Analysis (ATVA 2009)}",
 series       = "LNCS",
 volume       = "5799",
 publisher    = "Springer",
 address      = "{Macao SAR, China}",
 pages        = "337--351",
 doi          = "10.1007/978-3-642-04761-9\_25",
)
@article(sh:pipeline,
 author       = "J. Sawada and W. A. Hunt, Jr.",
 year         = "2002",
 title        = "{Verification of FM9801: An Out-of-Order Microprocessor Model with Speculative Execution, Exceptions, and Program-Modifying Capability}",
 journal      = "Formal Methods in Systems Design (FMSD)",
 volume       = "20",
 number       = "2",
 pages        = "187--222",
 doi          = "10.1023/A:1014122630277",
)
@inproceedings(tl:software-popl10,
 author       = "J. Tristan and X. Leroy",
 year         = "2010",
 title        = "{A Simple, Verified Validator for Software Pipelining}",
 editor       = "M. V. Hemenegildo and J. Palsberg",
 booktitle    = "{Proceedings of the $37$th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2010)}",
 pages        = "83--92",
 doi          = "10.1145/1706299.1706311",
)
@manual(legup,
 organization = "University of Toronto",
 year         = "{2013}",
 title        = "{LegUp Documentation Release 3.0}",
)
@article(velev05,
 author       = "M. N. Velev and R. E. Bryant",
 year         = "2005",
 title        = "{TLSim and EVC}: A Term-level Symbolic Simulator and An Efficient Decision Procedure for the Logic of Equality with Uninterpreted functions and Memories",
 journal      = "International Journal on Embedded Systems",
 pages        = "134--149",
 doi          = "10.1504/IJES.2005.008815",
)