@article(acl2s,
 author       = {P. Dillinger and P. Manolios and D. Vroon and J.S. Moore},
 year         = {2007},
 title        = {ACL2s: The ACL2 sedan},
 journal      = {Electronic Notes in Theoretical Computer Science - ENTCS},
 volume       = {174},
 doi          = {10.1016/j.entcs.2006.09.018},
)
@article(aprove,
 author       = {J. Giesl and C. Aschermann and M. Brockschmidt and et al.},
 year         = {2017},
 title        = {Analyzing Program Termination and Complexity Automatically with AProVE},
 journal      = {Journal of Automated Reasoning},
 volume       = {58},
 doi          = {10.1007/s10817-016-9388-y},
)
@book(ACL2,
 author       = {M. Kaufmann and P. Manolios and J.S. Moore},
 year         = {2000},
 title        = {Computer-Aided Reasoning: An Approach},
 publisher    = {Kluwer Academic},
 doi          = {10.1109/32.588534},
)
@article(buchi,
 author       = {O. Kupferman},
 year         = {2018},
 title        = {Automata Theory and Model Checking},
 journal      = {Handbook of Model Checking (2018)},
 doi          = {10.1007/978-3-319-10575-8_4},
)
@article(Lamport,
 author       = {L. Lamport},
 year         = {1974},
 title        = {A new solution of Dijkstra’s concurrent programming problem},
 journal      = {Communications of the ACM},
 volume       = {17},
 number       = {8},
 doi          = {10.1145/3335772.3335782},
)
@article(cav1,
 author       = {P. Manolios and K. Namjoshi and R. Sumners},
 year         = {1999},
 title        = {Linking model-checking and theorem-proving with well-founded bisimulations},
 journal      = {Proceedings of the 11th International Conference on Computer-Aided Verification (CAV 1999)},
 volume       = {1633},
 doi          = {10.1007/3-540-48683-6_32},
)
@article(ccg,
 author       = {P. Manolios and D. Vroon},
 year         = {2006},
 title        = {Termination Analysis with Calling Context Graphs.},
 journal      = {Proceedings of the 18th International Conference on Computer-Aided Verification (CAV 2006)},
 doi          = {10.1007/11817963_36},
)
@article(smtlink,
 author       = {Y. Peng and M. Greenstreet},
 year         = {2018},
 title        = {Smtlink 2.0},
 journal      = {Proceedings of 15th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2018)},
 doi          = {10.4204/EPTCS.280.11},
)
@article(RaySumners,
 author       = {S. Ray and R. Sumners},
 year         = {2013},
 title        = {Specification and Verification of Concurrent Programs Through Refinements},
 journal      = {Journal of Automated Reasoning},
 volume       = {51},
 number       = {3},
 doi          = {10.1007/s10817-012-9258-1},
)
@article(somenerd,
 author       = {R. Sumners},
 year         = {2017},
 title        = {Proof Reduction of Fair Stuttering Refinement of Asynchronous Systems and Applications},
 journal      = {Proceedings of 14th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2017)},
 doi          = {10.4204/EPTCS.249.6},
)
@article(ipasir,
 author       = {S. Swords},
 year         = {2018},
 title        = {Incremental SAT Library Integration Using Abstract Stobjs},
 journal      = {Proceedings of 15th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2018)},
 doi          = {10.4204/EPTCS.280.4},
)
@article(gl,
 author       = {S. Swords and J. Davis},
 year         = {2011},
 title        = {Bit-Blasting ACL2 Theorems},
 journal      = {Proceedings of 10th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2011)},
 doi          = {10.4204/EPTCS.70.7},
)