5 citations · 8 across the 7 of their papers we have counts for
7 papers
An Enumerative Embedding of the Python Type System in ACL2s
Samuel Xifaras, Panagiotis Manolios, Andrew T. Walter +1
Python is a high-level interpreted language that has become an industry standard in a wide variety of applications. In this paper, we take a first step towards using ACL2s to reaso…
An ACL2s Interface to Z3
Andrew T. Walter, Panagiotis Manolios
We present Lisp-Z3, an extension to the ACL2s systems programming framework (ASPF) that supports the use of the Z3 satisfiability modulo theories (SMT) solver. Lisp-Z3 allows one t…
Global Microprocessor Correctness in the Presence of Transient Execution
Andrew T. Walter, Konstantinos Athanasiou, Panagiotis Manolios
Correctness for microprocessors is generally understood to be conformance with the associated instruction set architecture (ISA). This is the basis for one of the most important ab…
Proving Calculational Proofs Correct
Andrew T. Walter, Ankit Kumar, Panagiotis Manolios
Teaching proofs is a crucial component of any undergraduate-level program that covers formal reasoning. We have developed a calculational reasoning format and refined it over sever…
Calculational Proofs in ACL2s
Andrew T. Walter, Ankit Kumar, Panagiotis Manolios
Teaching college students how to write rigorous proofs is a critical objective in courses that introduce formal reasoning. Over the course of several years, we have developed a mec…
Automated Grading of Automata with ACL2s
Ankit Kumar, Andrew Walter, Panagiotis Manolios
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-d…
A Reasoning Engine for the Gamification of Loop-Invariant Discovery
Andrew Walter, Seth Cooper, Panagiotis Manolios
We describe the design and implementation of a reasoning engine that facilitates the gamification of loop-invariant discovery. Our reasoning engine enables students, computational…