9 citations
- University of OxfordGB5 papers
- The University of Texas at AustinUS3 papers
- University of California San DiegoUS2 papers
- Forschungszentrum JülichDE1 paper
- Fujitsu (Japan)JP1 paper
- Integrated Software (United States)US1 paper
- Intel (United Kingdom)GB1 paper
- Northeastern UniversityUS1 paper
- Technische Universität BerlinDE1 paper
- Universidad del NoresteMX1 paper
- University of WyomingUS1 paper
22 papers
HiAER-Spike Software-Hardware Reconfigurable Platform for Event-Driven Neuromorphic Computing at Scale
Gwenevere Frank, Gopabandhu Hota, Keli Wang +12
In this work, we present HiAER-Spike, a modular, reconfigurable, event-driven neuromorphic computing platform designed to execute large spiking neural networks with up to 160 milli…
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…
A Proof of the Schröder-Bernstein Theorem in ACL2
Grant Jurgensen
The Schröder-Bernstein theorem states that, for any two sets P and Q, if there exists an injection from P to Q and an injection from Q to P, then there must exist a bijection betwe…
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…
Using Counterexample Generation and Theory Exploration to Suggest Missing Hypotheses
Ruben Gamboa, Panagiotis Manolios, Eric Smith +1
Newcomers to ACL2 are sometimes surprised that ACL2 rejects formulas that they believe should be theorems, such as (REVERSE (REVERSE X)) = X. Experienced ACL2 users will recognize…
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…