9 citations · 18 across the 5 of their papers we have counts for
5 papers · 1 filter
A Proof-Generating C Code Generator for ACL2 Based on a Shallow Embedding of C in ACL2
Alessandro Coglio
This paper describes a C code generator for ACL2 that recognizes ACL2 representations of C constructs, according to a shallow embedding of C in ACL2, and translates those represent…
A Complex Java Code Generator for ACL2 Based on a Shallow Embedding of ACL2 in Java
Alessandro Coglio
This paper describes a code generator that translates ACL2 constructs to corresponding Java constructs, according to a shallow embedding of ACL2 in Java. Starting from purely funct…
Isomorphic Data Type Transformations
Alessandro Coglio, Stephen Westfold
In stepwise derivations of programs from specifications, data type refinements are common. Many data type refinements involve isomorphic mappings between the more abstract and more…
Ethereum's Recursive Length Prefix in ACL2
Alessandro Coglio
Recursive Length Prefix (RLP) is used to encode a wide variety of data in Ethereum, including transactions. The work described in this paper provides a formal specification of RLP…
Adding 32-bit Mode to the ACL2 Model of the x86 ISA
Alessandro Coglio, Shilpi Goel
The ACL2 model of the x86 Instruction Set Architecture was built for the 64-bit mode of operation of the processor. This paper reports on our work to extend the model with support…