3 papers
cs.PL2025
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…
cs.LO2025
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…
cs.CR2025
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…