@misc(a2c,
 title        = {{A2C} : {Automatic Automata Checker}},
 howpublished = {\url{https://github.com/ankitku/A2C}},
)
@misc(acl2webpage,
 title        = {{ACL2} web-page},
 howpublished = {\url{https://www.cs.utexas.edu/users/moore/acl2/}},
)
@misc(acl2simage,
 title        = {{ACL2s} docker image},
 howpublished = {\url{https://hub.docker.com/r/atwalter/acl2s\@uscore .gradescope\@uscore .autograder/tags}},
)
@misc(acl2swebpage,
 title        = {{ACL2s} web-page},
 howpublished = {\url{http://acl2s.ccs.neu.edu/acl2s/doc/}},
)
@misc(gradescope,
 title        = {Gradescope},
 howpublished = {\url{https://www.gradescope.com}},
)
@inproceedings(alur2013automated,
 author       = {Rajeev Alur and Loris D’Antoni and Sumit Gulwani and Dileep Kini},
 year         = {2013},
 title        = {Automated Grading of {DFA} constructions},
 booktitle    = {International Joint Conference on Artificial Intelligence (IJCAI)},
 url          = {http://www.aaai.org/ocs/index.php/IJCAI/IJCAI13/paper/view/6759},
)
@inproceedings(acl2s11,
 author       = {Harsh Chamarthi and Peter C. Dillinger and Panagiotis Manolios and Daron Vroon},
 year         = {2011},
 title        = {The "{ACL2}" {Sedan Theorem Proving System}},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
 doi          = {10.1007/978-3-642-19835-9\_27},
)
@phdthesis(harsh-dissertation,
 author       = {Harsh Raju Chamarthi},
 year         = {2016},
 title        = {Interactive Non-theorem Disproving},
 school       = {Northeastern University},
 doi          = {10.17760/D20467205},
)
@inproceedings(cgen,
 author       = {Harsh Raju Chamarthi and Dillinger Peter C. and Matt Kaufmann and Panagiotis Manolios},
 year         = {2011},
 title        = {Integrating testing and interactive theorem proving},
 booktitle    = {International Workshop on the {ACL2} Theorem Prover and its Applications (ACL2)},
 doi          = {10.4204/EPTCS.70.1},
)
@inproceedings(defdata,
 author       = {Harsh Raju Chamarthi and Dillinger Peter C. and Panagiotis Manolios},
 year         = {2014},
 title        = {Data {Definitions} in the {ACL2} {Sedan}},
 booktitle    = {International Workshop on the {ACL2} Theorem Prover and its Applications (ACL2)},
 doi          = {10.4204/EPTCS.152.3},
)
@inproceedings(harsh-fmcad,
 author       = {Harsh Raju Chamarthi and Panagiotis Manolios},
 year         = {2011},
 title        = {Automated specification analysis using an interactive theorem prover},
 booktitle    = {International Conference on Formal Methods in Computer-Aided Design ({FMCAD})},
 url          = {http://dl.acm.org/citation.cfm?id=2157665},
)
@inproceedings(DillingerMVM07,
 author       = {Peter C. Dillinger and Panagiotis Manolios and Daron Vroon and J Strother Moore},
 year         = {2007},
 title        = {{ACL2s}: "{The} {ACL2} {Sedan}"},
 booktitle    = {International Conference on Software Engineering (ICSE)},
 doi          = {10.1016/j.entcs.2006.09.018},
)
@inproceedings(automatatutorv3,
 author       = {Loris D’Antoni and Martin Helfrich and Jan Kretinsky and Emanuel Ramneantu and Maximilian Weininger},
 year         = {2020},
 title        = {Automata Tutor v3},
 booktitle    = {International Conference on Computer Aided Verification (CAV)},
 doi          = {10.1007/978-3-030-53291-8\_1},
)
@inproceedings(dantoni2015how,
 author       = {Loris D’Antoni and Dileep Kini and Rajeev Alur and Sumit Gulwani and Mahesh Viswanathan and Björn Hartmann},
 year         = {2015},
 title        = {How Can Automatic Feedback Help Students Construct Automata?},
 booktitle    = {ACM Transactions on Computer-Human Interaction (TOCHI)},
 doi          = {10.1145/2723163},
)
@book(car,
 author       = {Matt Kaufmann and Panagiotis Manolios and J Strother Moore},
 year         = {2012},
 title        = {Computer-Aided Reasoning: An Approach},
 publisher    = {Springer US},
 url          = {https://link.springer.com/book/10.1007/978-1-4615-4449-4},
)
@inproceedings(acl2,
 author       = {Matt Kaufmann and J Strother Moore},
 title        = {{ACL2}: An industrial strength version of {Nqthm}},
 booktitle    = {Conference on Computer Assurance (COMPASS)},
 doi          = {10.1109/CMPASS.1996.507872},
)
@inproceedings(ManoliosVroon03,
 author       = {Panagiotis Manolios and Daron Vroon},
 year         = {2003},
 title        = {Algorithms for Ordinal Arithmetic},
 booktitle    = {19th International Conference on Automated Deduction ({CADE})},
 doi          = {10.1007/978-3-540-45085-6\_19},
)
@inproceedings(ManoliosVroon04,
 author       = {Panagiotis Manolios and Daron Vroon},
 year         = {2004},
 title        = {Integrating Reasoning about Ordinal Arithmetic into {ACL2}},
 booktitle    = {Formal Methods in Computer-Aided Design ({FMCAD})},
 doi          = {10.1007/978-3-540-30494-4\_7},
)
@article(MV05,
 author       = {Panagiotis Manolios and Daron Vroon},
 year         = {2005},
 title        = {{Ordinal Arithmetic: Algorithms and Mechanization}},
 journal      = {Journal of Automated Reasoning},
 doi          = {10.1007/s10817-005-9023-9},
)
@inproceedings(ccg,
 author       = {Panagiotis Manolios and Daron Vroon},
 year         = {2006},
 title        = {Termination Analysis with Calling Context Graphs},
 booktitle    = {Computer Aided Verification ({CAV})},
 doi          = {10.1007/11817963\_36},
)
@techreport(mcmillan2019increasing,
 author       = {Craig McMillan and Andy Crapo and Michael Durling and Meng Li and Abha Moitra and Panagiotis Manolios and Mark Stephens and Daniel Russell},
 year         = {2019},
 title        = {Increasing development assurance for system and software development with validation and verification using ASSERT™},
 type         = {Technical Report},
 institution  = {SAE Technical Paper},
 doi          = {10.4271/2019-01-1370},
)
@inproceedings(teaching-formal-languages,
 author       = {Mostafa Mohammed and Clifford A. Shaffer and Susan H. Rodger},
 year         = {2021},
 title        = {Teaching Formal Languages with Visualizations and Auto-Graded Exercises},
 booktitle    = {ACM Technical Symposium on Computer Science Education (SIGCSE TS)},
 doi          = {10.1145/3408877.3432398},
)
@inproceedings(moitra2018towards,
 author       = {Abha Moitra and Kit Siu and Andrew Crapo and Harsh Chamarthi and Michael Durling and Meng Li and Han Yu and Panagiotis Manolios and Michael Meiners},
 year         = {2018},
 title        = {Towards development of complete and conflict-free requirements},
 booktitle    = {2018 IEEE 26th International Requirements Engineering Conference (RE)},
 doi          = {10.1109/RE.2018.00036},
)
@article(norton2009algorithms,
 author       = {Daphne Norton},
 year         = {2009},
 title        = {Algorithms for testing equivalence of finite automata, with a grading tool for {JFLAP}},
 url          = {https://scholarworks.rit.edu/theses/6939},
)
@book(jflap-book,
 author       = {Susan H Rodger and Thomas W Finley},
 year         = {2006},
 title        = {JFLAP: an interactive formal languages and automata package},
 edition      = {{Computer Science ed.}},
 publisher    = {Jones and Bartlett Publishers, Inc.},
 url          = {https://www.jflap.org/jflapbook/jflapbook2006.pdf},
)
@inproceedings(opendsa,
 author       = {Clifford A. Shaffer},
 year         = {2016},
 title        = {Open{DSA}: An Interactive ETextbook for Computer Science Courses},
 booktitle    = {ACM Technical Symposium on Computing Science Education (SIGCSE TS)},
 doi          = {10.1145/2839509.2850505},
)
@inproceedings(enhancing-jflap,
 author       = {Vinay S. Shekhar and Anant Agarwalla and Akshay Agarwal and B. Nitish and Viraj Kumar},
 year         = {2014},
 title        = {Enhancing {JFLAP} with automata construction problems and automated feedback},
 booktitle    = {International Conference on Contemporary Computing (IC3)},
 doi          = {10.1109/IC3.2014.6897141},
)
@book(tocbook,
 author       = {Michael Sipser},
 year         = {2013},
 title        = {Introduction to the Theory of Computation},
 edition      = {{Third}},
 publisher    = {Course Technology},
)
@article(walter2021reasoning,
 author       = {Andrew Walter and Seth Cooper and Panagiotis Manolios},
 year         = {2021},
 title        = {A Reasoning Engine for the Gamification of Loop-Invariant Discovery},
 journal      = {arXiv preprint arXiv:2109.01121},
 doi          = {10.48550/arXiv.2109.01121},
)
@inproceedings(walter2019gamification,
 author       = {Andrew T Walter and Benjamin Boskin and Seth Cooper and Panagiotis Manolios},
 year         = {2019},
 title        = {Gamification of Loop-Invariant Discovery from Code},
 booktitle    = {Proceedings of the AAAI Conference on Human Computation and Crowdsourcing},
 doi          = {10.1609/hcomp.v7i1.5277},
)
@inproceedings(Walter2022,
 author       = {Andrew T Walter and David Greve and Panagiotis Manolios},
 year         = {2022},
 title        = {Enumerative Data Types with Constraints},
 booktitle    = {Conference on Formal Methods in Computer-Aided Design--FMCAD 2022},
 doi          = {10.34727/2022/isbn.978-3-85448-053-2\@uscore .25},
)
@inproceedings(interface,
 author       = {Andrew T. Walter and Panagiotis Manolios},
 year         = {2022},
 title        = {ACL2s Systems Programming},
 booktitle    = {International Workshop on the {ACL2} Theorem Prover and its Applications (ACL2)},
 doi          = {10.4204/EPTCS.359.12},
)