9 citations · 43 across the 13 of their papers we have counts for
13 papers
A Formalization of the Yul Language and Some Verified Yul Code Transformations
Alessandro Coglio, Eric McCarthy
Yul is an intermediate language used in the compilation of the Solidity programming language for Ethereum smart contracts. The compiler applies customizable sequences of transforma…
Formal Verification of Blockchain Nonforking in DAG-Based BFT Consensus with Dynamic Stake
Alessandro Coglio, Eric McCarthy
Blockchain consensus protocols enable participants to agree on consistent views of the blockchain that may be ahead or behind relative to each other but do not fork into different…
Formal Verification of Zero-Knowledge Circuits
Alessandro Coglio, Eric McCarthy, Eric W. Smith
Zero-knowledge circuits are sets of equality constraints over arithmetic expressions interpreted in a prime field; they are used to encode computations in cryptographic zero-knowle…
Proceedings of the 18th International Workshop on the ACL2 Theorem Prover and Its Applications
Alessandro Coglio, Sol Swords
This volume contains the proceedings of the Eighteenth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2023), a two-day workshop held at the University…
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…