The OMRS project: state of the art. - Fausto Giunchiglia; Piergiorgio Bertoli; Alessandro Coglio (WRLA, 1998)

An Architecture for Emotional Agents. - Antonio Camurri; Alessandro Coglio (IEEE Multim., 1998)

The control component of open mechanized reasoning systems. - Alessandro Armando; Alessandro Coglio; Fausto Giunchiglia (Calculemus, 1999)

Composing and Controlling Search in Reasoning Theories Using Mappings. - Alessandro Coglio; Fausto Giunchiglia; José Meseguer 001; Carolyn L. Talcott (FroCoS, 2000)

A formal specification of JavaTM class loading. - Zhenyu Qian; Allen Goldberg; Alessandro Coglio (OOPSLA, 2000)

Type safety in the JVM: some problems in Java 2 SDK 1.2 and proposed solutions. - Alessandro Coglio; Allen Goldberg (Concurr. Comput. Pract. Exp., 2001)

The Control Layer in Open Mechanized Reasoning Systems: Annotations and Tactics. - Alessandro Armando; Alessandro Coglio; Fausto Giunchiglia; Silvio Ranise (J. Symb. Comput., 2001)

Improving the official specification of Java bytecode verification. - Alessandro Coglio (Concurr. Comput. Pract. Exp., 2003)

Formal Techniques for Java-Like Programs (FTfJP). - Alessandro Coglio; Marieke Huisman; Joseph Kiniry; Peter Müller 001; Erik Poll (ECOOP Workshops, 2004)

Simple verification technique for complex Java bytecode subroutines. - Alessandro Coglio (Concurr. Pract. Exp., 2004)

A Constructive Approach to Correctness, Exemplified by a Generator for Certified Java Card Applets. - Alessandro Coglio; Cordell Green (VSTTE, 2005)

Checking Access to Protected Members in the Java Virtual Machine. - Alessandro Coglio (J. Object Technol., 2005)

Roadmap for enhanced languages and methods to aid verification. - 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 001; Simon L. Peyton Jones; Murali Sitaraman; Douglas R. Smith; et al. (GPCE, 2006)

Two Demonstrations of Economical EAL5+ Development for Tokeneer. - John Anton; Martin Croxford; Alessandro Coglio; Janet Barnes; Randy Johnson; Tim Kremann (ISSSE, 2006)

Pop-Refinement. - Alessandro Coglio (Arch. Formal Proofs, 2014)

Distributed Real-Time Managed Systems: A Model-Driven Distributed Secure Information Architecture Platform for Managed Embedded Systems. - Tihamer Levendovszky; Abhishek Dubey; William Otte; Daniel Balasubramanian; Alessandro Coglio; Sandor Nyako; William Emfinger; Pranav Srinivas Kumar; Aniruddha S. Gokhale; Gabor Karsai (IEEE Softw., 2014)

Android Platform Modeling and Android App Verification in the ACL2 Theorem Prover. - Eric Smith; Alessandro Coglio (VSTTE, 2015)

Second-Order Functions and Theorems in ACL2. - Alessandro Coglio (ACL2, 2015)

AutoRand: Automatic Keyword Randomization to Prevent Injection Attacks. - Jeff H. Perkins; Jordan Eikenberry; Alessandro Coglio; Daniel Willenson; Stelios Sidiroglou-Douskos; Martin C. Rinard (DIMVA, 2016)

A Versatile, Sound Tool for Simplifying Definitions. - Alessandro Coglio; Matt Kaufmann; Eric Whitman Smith (ACL2, 2017)

A Formalization of the ABNF Notation and a Verified Parser of ABNF Grammars. - Alessandro Coglio (VSTTE, 2018)

A Simple Java Code Generator for ACL2 Based on a Deep Embedding of ACL2 in Java. - Alessandro Coglio (ACL2, 2018)

Adding 32-bit Mode to the ACL2 Model of the x86 ISA. - Alessandro Coglio; Shilpi Goel (ACL2, 2018)

Comprehensive Java Metadata Tracking for Attack Detection and Repair. - Jeff H. Perkins; Jordan Eikenberry; Alessandro Coglio; Martin C. Rinard (DSN, 2020)

Ethereum's Recursive Length Prefix in ACL2. - Alessandro Coglio (ACL2, 2020)

Isomorphic Data Type Transformations. - Alessandro Coglio; Stephen J. Westfold (ACL2, 2020)

Towards Model-Based Intent-Driven Adaptive Software. - Daniel Balasubramanian; Alessandro Coglio; Abhishek Dubey; Gabor Karsai (ISoLA, 2021)

Leo: A Programming Language for Formally Verified, Zero-Knowledge Applications. - Collin Chin; Howard Wu; Raymond Chu; Alessandro Coglio; Eric McCarthy; Eric Smith (IACR Cryptol. ePrint Arch., 2021)

Syntheto: A Surface Language for APT and ACL2. - Alessandro Coglio; Eric McCarthy; Stephen J. Westfold; Daniel Balasubramanian; Abhishek Dubey; Gabor Karsai (ACL2, 2022)

A Complex Java Code Generator for ACL2 Based on a Shallow Embedding of ACL2 in Java. - Alessandro Coglio (ACL2, 2022)

A Proof-Generating C Code Generator for ACL2 Based on a Shallow Embedding of C in ACL2. - Alessandro Coglio (ACL2, 2022)

Formal Verification of Zero-Knowledge Circuits. - Alessandro Coglio; Eric McCarthy; Eric Whitman Smith (ACL2, 2023)

Compositional Formal Verification of Zero-Knowledge Circuits. - Alessandro Coglio; Eric McCarthy; Eric Smith; Collin Chin; Pranav Gaddamadugu; Michel Dellepere (IACR Cryptol. ePrint Arch., 2023)

Formal Verification of Blockchain Nonforking in DAG-Based BFT Consensus with Dynamic Stake. - Alessandro Coglio; Eric McCarthy (CoRR, 2025)

A Formalization of the Yul Language and Some Verified Yul Code Transformations. - Alessandro Coglio; Eric McCarthy (CoRR, 2025)