4 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…
A Formalization of the Correctness of the Floodsub Protocol
Ankit Kumar, Panagiotis Manolios
Floodsub is a simple, robust and popular peer-to-peer publish/subscribe (pubsub) protocol, where nodes can arbitrarily leave or join the network, subscribe to or unsubscribe from 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…