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.

翻译：几乎所有计算机科学专业都要求学生修读计算理论课程（ToC），该课程涵盖多种计算模型，如有限自动机、下推自动机和图灵机。计算理论课程通常布置需要纸笔解答的作业，这类作业的批改耗时较长，因此学生通常在完成作业一周后才能收到反馈。我们提出了自动自动机检查器（A2C），这是一个开源库，允许用户使用与标准教科书定义相似的规范构建可执行的自动机模型。此类构造可通过语义等价性检查、属性验证和测试用例轻松进行推理。教师可以便捷地以自身构造形式指定标准答案。A2C能够自动检测学生答案与教师答案之间的语义等价性，并即时生成可操作反馈，帮助学生更好地理解课程内容。学生可下载并在本地使用A2C，该工具也可集成至Gradescope等学习管理系统（LMS）中，自动批改学生提交的作业并生成反馈。A2C基于ACL2s交互式定理证明器，该证明器提供用于陈述、证明及反驳属性的高级方法。由于反馈完全自动化，A2C可大规模部署并集成至大型开放式在线课程中。