  Almost all Computer Science programs require students to take a course on the
Theory of Computation (ToC) which covers various models of computation such as
finite automata, push-down automata and Turing machines. ToC courses tend to
give assignments that require paper-and-pencil solutions. Grading such
assignments takes time, so students typically receive feedback for their
solutions more than a week after they complete them. We present the Automatic
Automata Checker (A2C), an open source library that enables one to construct
executable automata using definitions that mimic those found in standard
textbooks. Such constructions are easy to reason about using semantic
equivalence checks, properties and test cases. Instructors can conveniently
specify solutions in the form of their own constructions. A2C can check for
semantic equivalence between student and instructor solutions and can
immediately generate actionable feedback, which helps students better
understand the material. A2C can be downloaded and used locally by students as
well as integrated into Learning Management Systems (LMS) like Gradescope to
automatically grade student submissions and generate feedback. A2C is based on
the ACL2s interactive theorem prover, which provides advanced methods for
stating, proving and disproving properties. Since feedback is automatic, A2C
can be deployed at scale and integrated into massively open online courses.
