Alessandro Coglio

36 papers A 2B 2C 1Journal 11Unranked 19

Year	Rank	Type	Title / Venue / Authors
2025	—	`conf`	A Formalization of the Yul Language and Some Verified Yul Code Transformations. ACL2 Alessandro Coglio, Eric McCarthy
2025	J	`jnl`	Formal Verification of Blockchain Nonforking in DAG-Based BFT Consensus with Dynamic Stake. CoRR Alessandro Coglio, Eric McCarthy
2023	J	`jnl`	Compositional Formal Verification of Zero-Knowledge Circuits. IACR Cryptol. ePrint Arch. Alessandro Coglio, Eric McCarthy, Eric Smith, Collin Chin, Pranav Gaddamadugu, Michel Dellepere
2023	—	`conf`	Formal Verification of Zero-Knowledge Circuits. ACL2 Alessandro Coglio, Eric McCarthy, Eric Whitman Smith
2023	—	`ed.`	Proceedings of the 18th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, TX, USA and online, November 13-14, 2023. ACL2 Alessandro Coglio, Sol Swords
2022	—	`conf`	A Complex Java Code Generator for ACL2 Based on a Shallow Embedding of ACL2 in Java. ACL2 Alessandro Coglio
2022	—	`conf`	A Proof-Generating C Code Generator for ACL2 Based on a Shallow Embedding of C in ACL2. ACL2 Alessandro Coglio
2022	—	`conf`	Syntheto: A Surface Language for APT and ACL2. ACL2 Alessandro Coglio, Eric McCarthy, Stephen J. Westfold, Daniel Balasubramanian, Abhishek Dubey, Gabor Karsai
2021	J	`jnl`	Leo: A Programming Language for Formally Verified, Zero-Knowledge Applications. IACR Cryptol. ePrint Arch. Collin Chin, Howard Wu, Raymond Chu, Alessandro Coglio, Eric McCarthy, Eric Smith
2021	C	`conf`	Towards Model-Based Intent-Driven Adaptive Software. ISoLA Daniel Balasubramanian, Alessandro Coglio, Abhishek Dubey, Gabor Karsai
2020	A	`conf`	Comprehensive Java Metadata Tracking for Attack Detection and Repair. DSN Jeff H. Perkins, Jordan Eikenberry, Alessandro Coglio, Martin C. Rinard
2020	—	`conf`	Ethereum's Recursive Length Prefix in ACL2. ACL2 Alessandro Coglio
2020	—	`conf`	Isomorphic Data Type Transformations. ACL2 Alessandro Coglio, Stephen J. Westfold
2018	—	`conf`	A Formalization of the ABNF Notation and a Verified Parser of ABNF Grammars. VSTTE Alessandro Coglio
2018	—	`conf`	A Simple Java Code Generator for ACL2 Based on a Deep Embedding of ACL2 in Java. ACL2 Alessandro Coglio
2018	—	`conf`	Adding 32-bit Mode to the ACL2 Model of the x86 ISA. ACL2 Alessandro Coglio, Shilpi Goel
2017	—	`conf`	A Versatile, Sound Tool for Simplifying Definitions. ACL2 Alessandro Coglio, Matt Kaufmann, Eric Whitman Smith
2016	B	`conf`	AutoRand: Automatic Keyword Randomization to Prevent Injection Attacks. DIMVA Jeff H. Perkins, Jordan Eikenberry, Alessandro Coglio, Daniel Willenson, Stelios Sidiroglou-Douskos, Martin C. Rinard
2015	—	`conf`	Android Platform Modeling and Android App Verification in the ACL2 Theorem Prover. VSTTE Eric Smith, Alessandro Coglio
2015	—	`conf`	Second-Order Functions and Theorems in ACL2. ACL2 Alessandro Coglio
2014	J	`jnl`	Distributed Real-Time Managed Systems: A Model-Driven Distributed Secure Information Architecture Platform for Managed Embedded Systems. IEEE Softw. Tihamer Levendovszky, Abhishek Dubey, William Otte, Daniel Balasubramanian, Alessandro Coglio, Sandor Nyako, William Emfinger, Pranav Srinivas Kumar, Aniruddha S. Gokhale, Gabor Karsai
2014	J	`jnl`	Pop-Refinement. Arch. Formal Proofs Alessandro Coglio
2006	B	`conf`	Roadmap for enhanced languages and methods to aid verification. GPCE Gary T. Leavens, Jean-Raymond Abrial, Don S. Batory, Michael J. Butler, Alessandro Coglio, Kathi Fisler, Eric C. R. Hehner, Cliff B. Jones, Dale Miller, Simon L. Peyton Jones, Murali Sitaraman, Douglas R. Smith, Aaron Stump
2006	—	`conf`	Two Demonstrations of Economical EAL5+ Development for Tokeneer. ISSSE John Anton, Martin Croxford, Alessandro Coglio, Janet Barnes, Randy Johnson, Tim Kremann
2005	—	`conf`	A Constructive Approach to Correctness, Exemplified by a Generator for Certified Java Card Applets. VSTTE Alessandro Coglio, Cordell Green
2005	J	`jnl`	Checking Access to Protected Members in the Java Virtual Machine. J. Object Technol. Alessandro Coglio
2004	—	`conf`	Formal Techniques for Java-Like Programs (FTfJP). ECOOP Workshops Alessandro Coglio, Marieke Huisman, Joseph Kiniry, Peter Müller, Erik Poll
2004	J	`jnl`	Simple verification technique for complex Java bytecode subroutines. Concurr. Pract. Exp. Alessandro Coglio
2003	J	`jnl`	Improving the official specification of Java bytecode verification. Concurr. Comput. Pract. Exp. Alessandro Coglio
2001	J	`jnl`	The Control Layer in Open Mechanized Reasoning Systems: Annotations and Tactics. J. Symb. Comput. Alessandro Armando, Alessandro Coglio, Fausto Giunchiglia, Silvio Ranise
2001	J	`jnl`	Type safety in the JVM: some problems in Java 2 SDK 1.2 and proposed solutions. Concurr. Comput. Pract. Exp. Alessandro Coglio, Allen Goldberg
2000	A	`conf`	A formal specification of Java OOPSLA Zhenyu Qian, Allen Goldberg, Alessandro Coglio
2000	—	`conf`	Composing and Controlling Search in Reasoning Theories Using Mappings. FroCoS Alessandro Coglio, Fausto Giunchiglia, José Meseguer, Carolyn L. Talcott
1999	—	`conf`	The control component of open mechanized reasoning systems. Calculemus Alessandro Armando, Alessandro Coglio, Fausto Giunchiglia
1998	J	`jnl`	An Architecture for Emotional Agents. IEEE Multim. Antonio Camurri, Alessandro Coglio
1998	—	`conf`	The OMRS project: state of the art. WRLA Fausto Giunchiglia, Piergiorgio Bertoli, Alessandro Coglio