Gamification of Loop-Invariant Discovery from Code. - Andrew T. Walter; Benjamin Boskin; Seth Cooper; Panagiotis Manolios (HCOMP, 2019)

A Reasoning Engine for the Gamification of Loop-Invariant Discovery. - Andrew T. Walter; Seth Cooper; Panagiotis Manolios (CoRR, 2021)

Enumerative Data Types with Constraints. - Andrew T. Walter; David A. Greve; Panagiotis Manolios (FMCAD, 2022)

ACL2s Systems Programming. - Andrew T. Walter; Panagiotis Manolios (ACL2, 2022)

Automated Grading of Automata with ACL2s. - Ankit Kumar; Andrew T. Walter; Panagiotis Manolios (ThEdu@FLoC, 2022)

Calculational Proofs in ACL2s. - Andrew T. Walter; Ankit Kumar; Panagiotis Manolios (CoRR, 2023)

Proving Calculational Proofs Correct. - Andrew T. Walter; Ankit Kumar; Panagiotis Manolios (ACL2, 2023)

Global Microprocessor Correctness in the Presence of Transient Execution. - Andrew T. Walter; Konstantinos Athanasiou; Panagiotis Manolios (CoRR, 2025)

An ACL2s Interface to Z3. - Andrew T. Walter; Panagiotis Manolios (CoRR, 2025)

An Enumerative Embedding of the Python Type System in ACL2s. - Samuel Xifaras; Panagiotis Manolios; Andrew T. Walter; William Robertson 002 (CoRR, 2025)