@article(cegar,
 author       = {Edmund Clarke and Orna Grumberg and Somesh Jha and Yuan Lu and Helmut Veith},
 year         = {2003},
 title        = {Counterexample-guided Abstraction Refinement for Symbolic Model Checking},
 journal      = {J. ACM},
 volume       = {50},
 number       = {5},
 pages        = {752--794},
 url          = {http://doi.acm.org/10.1145/876638.876643},
)
@inproceedings(AbstractInterpretation,
 author       = {Patrick Cousot and Radhia Cousot},
 year         = {1977},
 title        = {Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints},
 booktitle    = {Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages},
 series       = {POPL '77},
 publisher    = {ACM},
 address      = {New York, NY, USA},
 pages        = {238--252},
 url          = {http://doi.acm.org/10.1145/512950.512973},
)
@article(AbstractIntervals,
 author       = {Patrick Cousot and Radhia Cousot},
 year         = {1977},
 title        = {Static Determination of Dynamic Properties of Generalized Type Unions},
 journal      = {SIGPLAN Not.},
 volume       = {12},
 number       = {3},
 pages        = {77--94},
 url          = {http://doi.acm.org/10.1145/390017.808314},
)
@inproceedings(JKind,
 author       = {Andrew Gacek and John Backes and Mike Whalen and Lucas G. Wagner and Elaheh Ghassabani},
 year         = {2018},
 title        = {The JKind Model Checker},
 booktitle    = {Computer Aided Verification - 30th International Conference, {CAV} 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part {II}},
 pages        = {20--27},
 url          = {https://doi.org/10.1007/978-3-319-96142-2\_3},
)
@inproceedings(nary,
 author       = {David Greve},
 year         = {2006},
 title        = {Parameterized Congruences in ACL2},
 booktitle    = {Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and Its Applications},
 series       = {ACL2 '06},
 publisher    = {ACM},
 address      = {New York, NY, USA},
 pages        = {28--34},
 url          = {http://doi.acm.org/10.1145/1217975.1217981},
)
@inproceedings(assuming,
 author       = {David Greve},
 year         = {2009},
 title        = {Assuming Termination},
 booktitle    = {Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and Its Applications},
 series       = {ACL2 '09},
 publisher    = {ACM},
 address      = {New York, NY, USA},
 pages        = {114--122},
 url          = {http://doi.acm.org/10.1145/1637837.1637856},
)
@misc(rump,
 author       = {David Greve},
 year         = {2017},
 title        = {{Generalization Correctness}},
 howpublished = {\url{http://www.cs.utexas.edu/users/moore/acl2/workshop-2017/slides-rump/greve-ACL2-2017.pdf}},
)
@misc(FuzzM,
 author       = {David Greve},
 year         = {2018},
 title        = {{FuzzM: Fuzzing with Models}},
 howpublished = {\url{https://github.com/collins-research/FuzzM}},
)
@inproceedings(defung,
 author       = {David Greve and Konrad Slind},
 year         = {2013},
 title        = {A Step-Indexing Approach to Partial Functions},
 editor       = {Ruben Gamboa and Jared Davis},
 booktitle    = {{\rm Proceedings International Workshop on the} ACL2 Theorem Prover and its Applications, {\rm Laramie, Wyoming, USA , May 30-31, 2013}},
 series       = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {114},
 publisher    = {Open Publishing Association},
 pages        = {42--53},
 doi          = {10.4204/EPTCS.114.4},
)
@article(lustre:ieee,
 author       = {N. Halbwachs and P. Caspi and P. Raymond and D. Pilaud},
 year         = {1991},
 title        = {The synchronous data flow programming language LUSTRE},
 journal      = {Proceedings of the IEEE},
 volume       = {79},
 number       = {9},
 pages        = {1305--1320},
 doi          = {10.1109/5.97300},
)
@article(DBLP:Octagon,
 author       = {Antoine Min{\'e}},
 year         = {2006},
 title        = {The Octagon Abstract Domain},
 journal      = {Higher Order Symbol. Comput.},
 volume       = {19},
 number       = {1},
 pages        = {31--100},
 url          = {http://dx.doi.org/10.1007/s10990-006-8609-1},
)
@inproceedings(WelpQFBV,
 author       = {Tobias Welp and Andreas Kuehlmann},
 year         = {2013},
 title        = {{QF_BV} Model Checking with Property Directed Reachability},
 booktitle    = {Proceedings of the Conference on Design, Automation and Test in Europe},
 series       = {DATE '13},
 publisher    = {EDA Consortium},
 address      = {San Jose, CA, USA},
 pages        = {791--796},
 url          = {http://dl.acm.org/citation.cfm?id=2485288.2485480},
)