Alessandro Coglio
Contact
coglio@K.E, where K=kestrel and E=edu
GitHub: acoglio
LinkedIn: Alessandro Coglio
Bio
I’m a Principal Scientist at Kestrel Institute, which I joined in 1998. I’m also a Cofounder of, Board Director of, and Principal Software Engineer at Kestrel Technology LLC (a spinoff of Kestrel Institute). My current and past work at Kestrel includes:

Development of techniques for program specification, refinement, transformation, synthesis, and verification [11, 8, 6, 4, 2, 16, 14]. Implementation in ACL2 [8, 6, 4, 2]. Application to numerous examples in a variety of domains. Also see the APT, Hyperproperties, DerivationMiner, and Specware project pages.

Formal specification of Bitcoin and Ethereum in ACL2 [1]. Also see the ACL2 Ethereum project page.

Formalization of the syntax and semantics of ABNF (Augmented BackusNaur Form), development of a verified parser of ABNF grammars, and development of operations on ABNF grammars, using ACL2 [5].

Contributions to the Ethereum Yellow Paper. Membership in the Ethereum Yellow Paper Maintainers Team and in the Ethereum Specification Maintainers Team.

Extension to 32bit mode of an opensource formal model in ACL2 of the x86 Instruction Set Architecture [3].

Formal specification of a resolutionbased theorem prover using ACL2, and generation of verified specialized implementations using APT. Also see the CASE project page.

Formal specification and verification of the type safety mechanisms of the Java Virtual Machine [33, 28, 30, 29, 25, 27, 22, 23, 18, 19, 15, 17] (see acknowledgment in the Preface to the Java SE 7 Edition of the Java Virtual Machine Specification). Formal specification, using Specware and Isabelle, of the Java Card Runtime Environment (including GlobalPlatform) and of runtime monitors that provably enforce information flow policies in the Java Card Runtime Environment. Development of an implementation in C of the Java Card Runtime Environment, based on the formal specification, for a commercial smart card chip. Automatic generation of provably correct Java Card applets from higherlevel specifications written in a domainspecific language for smart cards [24, 21, 20, 16]. Also see the Java, JCRE, and AutoSmart project pages.

Contributions to Java Specification Request 202 (Java Class File Specification Update), as member of the Expert Group.

Design, formal specification in Isabelle, and implementation in C of mechanisms to enforce multidomain multilevel security, and their application to an information architecture for distributed embedded systems such as fractionated satellites [13, 12, 10]. Also see the F6 project page.

Formal verification of Android apps using ACL2 [9]. Also see the APAC project page.

Formal specification and refinement, in Specware, of the control software of Tokeneer, an access control system for secure enclaves based on smart card and biometric authentication.

Formal specification and verification of a virtual Trusted Platform Module in Specware and PVS. Also see the vTPM project page.

Automatic removal of security vulnerabilities from Java bytecode via analysis, confinement, and diversification [7]. Also see the VIBRANCE project page.

Contributions to the Isabelle library and Archive of Formal Proofs [11].
Before joining Kestrel, I was a Consulting Researcher at the Mechanized Reasoning Group and the Laboratory of Musical Informatics at the Department of Informatics, Systems, and Telecommunications of University of Genoa. My work there includes:

Formalism to specify control strategies of theorem provers and its application to the NQTHM theorem prover [46, 44, 36, 35, 32, 31, 26] (this was also the topic of my thesis).

Formalization of new classes of highlevel Petri nets, implementation in C++ of an executor for one of those classes, development of a hybrid architecture (Petri nets + expert systems) for plant simulation, and development of a formalism for controlling discrete event systems [45, 43, 42, 39, 38, 37].
I received a degree in Informatics Engineering from University of Genoa in 1996. My thesis was in collaboration with ITCIRST (now FBK) (Trento, Italy) and Stanford University (Palo Alto, California), where I spent a couple of months just after graduating. As of 2011, I’m also a Stanford Certified Project Manager.
During my middle and highschool years, I designed and implemented some video games in Assembly on the glorious Commodore 64 first, then on the alsoglorious Commodore Amiga. During my university years, I designed and implemented a graphical generator of hypertextual adventure games in Plus (a HyperCardlike system for Windows). Currently, I’m interested in investigating formal specification and refinement of video games.
In case it wasn’t clear already, I’m from Italy, more precisely Genoa.
Publications

Ethereum's Recursive Length Prefix in ACL2
May 2020
16th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL22020)
{Description of a formal specification of RLP encoding and a verified implementation of RLP decoding, all developed in ACL2. This web version of the paper is identical to the one published at EPTCS, with the addition of an appendix about ACL2 to make the paper more selfcontained. Supersedes Kestrel Institute Technical Report Ethereum’s Recursive Length Prefix in ACL2 of August 2019.} 
Isomorphic Data Type Transformations
(with Stephen Westfold)
May 2020
16th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL22020)
{Description of methods and tools to isomorphically transform data, for both program synthesis and program analysis, realized in the ACL2 theorem provers, but more generally applicable. The tools are part of APT.} 
Adding 32bit Mode to the ACL2 Model of the x86 ISA
(with Shilpi Goel)
November 2018
15th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL22018)
{Description of how the x86 formal model in ACL2 was extended from 64bit mode to 32bit mode.} 
A Simple Java Code Generator for ACL2 Based on a Deep Embedding of ACL2 in Java
November 2018
15th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL22018)
{Description of two tools: AIJ (= ACL2 In Java) and ATJ (= ACL2 To Java). AIJ is an interpreter, written in Java, of an executable subset of ACL2. ATJ is a code generator that translates ACL2 code into a Java representation in AIJ. ATJ is based on AIJ, while AIJ can be used independently from ATJ.} 
A Formalization of the ABNF Notation and a Verified Parser of ABNF Grammars
July 2018
10th International Conference on Verified Software: Tools, Techniques, and Experiments (VSTTE)
Lecture Notes in Computer Science (LNCS), Number 11294, pages 177195
{Description of (i) a formalization of the syntax and semantics of the ABNF (Augmented BackusNaur Form) notation and (ii) a verified parser that turns ABNF grammar text into a formal representation usable in declarative specifications of parsers of ABNFspecified languages. Supersedes Kestrel Institute Technical Report ABNF in ACL2 of July 2017.} 
A Versatile, Sound Tool for Simplifying Definitions
(with Matt Kaufmann and Eric Smith)
May 2017
14th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL22017)
{Description of a tool to transform ACL2 functions definitions into simplified function definitions and to generate a proof of equivalence between old and new functions that is checked by ACL2. The tool is useful in both program synthesis and analysis. The tool is part of APT.} 
AutoRand: Automatic Keyword Randomization to Prevent Injection Attacks
(with Jeff Perkins, Jordan Eikenberry, Daniel Willenson, Stelios SidiroglouDouskos, and Martin Rinard)
July 2016
13th Conference on Detection of Intrusions and Malware & Vulnerability Assessment (DIMVA)
{Description of an approach to automatically harden Java applications against injection attacks by randomizing the injectable keywords within the application.} 
SecondOrder Functions and Theorems in ACL2
October 2015
13th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL22015), pages 1733
{Description of SOFT (= SecondOrder Functions and Theorems), an ACL2 library to mimic secondorder functions and theorems in the firstorder logic of ACL2; example of use of SOFT in the shallow poprefinement approach to program refinement. Shallow poprefinement is a form of poprefinement [11] in which the programs predicated upon are shallowly embedded functions of the logic of the theorem prover, instead of deeply embedded programs of a programming language.} 
Android Platform Modeling and Android App Verification in the ACL2 Theorem Prover (with Eric Smith)
July 2015
7th International Conference on Verified Software: Tools, Techniques, and Experiments (VSTTE)
Lecture Notes in Computer Science (LNCS), Number 9593, pages 183201
{Description of a formal model of a subset of the Android platform and of an approach to formally verify the functional correctness of Android apps using the model.} 
Establishing Secure Interactions Across Distributed Applications in Satellite Clusters
(with Subhav Pradhan, William Emfinger, Abhishek Dubey, William Otte, Daniel Balasubramanian, Aniruddha Gokhale, and Gabor Karsai)
September 2014
5th IEEE International Conference on Space Mission Challenges in Information Technology (SMCIT), pages 6774
{More detailed description of the secure communications mechanisms in the architecture overviewed in [13] and [12].} 
PopRefinement
July 2014
Archive of Formal Proofs
{Description of an approach to refinement in which specifications are predicates over programs and refinement is inclusion of predicates; two simple examples are developed in Isabelle/HOL, one of which features the preservation of hyperproperties (which are predicates over sets of traces). Supersedes Kestrel Institute Technical Report Refinement as Inclusion of Predicates over Programs of July 2012. Supersedes Kestrel Institute Technical Report PopRefinement of November 2013. Supersedes Kestrel Institute Technical Report A Simple Example of PopRefinement in Isabelle/HOL of November 2013. Supersedes Kestrel Institute Technical Report A Simple Example of PopRefinement and Hyperproperties in Isabelle/HOL of January 2014.} 
DREMS: A ModelDriven Distributed Secure Information Architecture Platform for Managed Embedded Systems
(with Tihamer Levendovszky, Abhishek Dubey, William R. Otte, Daniel Balasubramanian, Sandor Nyako, William Emfinger, Pranav Kumar, Aniruddha Gokhale, and Gabor Karsai)
March/April 2014
IEEE Software, Volume 31, Number 2, pages 6269
{Overview of a multilevel secure, faulttolerant information architecture, and associated modelbased development tools, for embedded systems. An earlier version of this architecure, tailored to fractionated satellites, is described in [13].} 
A Software Platform for Fractionated Spacecraft
(with Abhishek Dubey, William Emfinger, Aniruddha Gokhale, Gabor Karsai, William Otte, Jeffrey Parson, Csanád Szabó, Eric Smith, and Prasanta Bose)
March 2012
2012 IEEE Aerospace Conference, pages 120
{Overview of a multilevel secure, faulttolerant information architecture, and associated modelbased development tools, for fractionated satellites. Also applicable to other kinds of distributed embedded systems. A later version of this architecture, for general embedded systems, is described in [12].} 
Roadmap for Enhanced Languages and Methods to Aid Verification
(with Gary Leavens, JeanRaymond Abrial, Don Batory, Michael Butler, Kathi Fisler, Eric Hehner, Cliff Jones, Dale Miller, Simon PeytonJones, Murali Sitaraman, Doug Smith, and Aaron Stump)
October 2006
5th International Conference on Generative Programming and Component Engineering (GPCE), pages 221236
{Roadmap for research to further the goal of verified software.} 
Checking Access to Protected Members in the Java Virtual Machine
October 2005
Journal of Object Technology, Volume 4, Number 8, pages 5576
{Detailed analysis of the requirements on protected member access in the Java Virtual Machine and how to check them; examples of incorrect checking in Sun’s Java 2 SDK version 1.4. A shorter version is [19]. Supersedes Kestrel Institute Technical Report Checking Access to Protected Members in the Java Virtual Machine of February 2004.} 
A Constructive Approach to Correctness, Exemplified by a Generator for Certified Java Card Applets
(with Cordell Green)
October 2005
1st IFIP TC 2/WG 2.3 Conference on Verified Software: Tools, Techniques, and Experiments (VSTTE)
Lecture Notes in Computer Science (LNCS), Number 4171, pages 5763
{Position paper describing an approach to synthesize correct software that can be independently certified. A generator of Java Card applets is presented as an example of the approach.} 
Formal Techniques for JavaLike Programs (FTfJP)
(with Marieke Huisman, Joseph Kiniry, Peter Müller, and Erik Poll)
January 2005
ObjectOriented Technology. ECOOP 2004 Workshop Reader Lecture Notes in Computer Science (LNCS), Number 3344, pages 7683
{Report on the workshop.} 
Simple Verification Technique for Complex Java Bytecode Subroutines
June 2004
Concurrency and Computation: Practice and Experience, Volume 16, Issue 7, pages 647670
{Definition of a simple and powerful technique to verify Java bytecode with subroutines, which arguably accepts all the bytecode generated by Java compilers. The technique is overviewed in [23]. Supersedes Kestrel Institute Technical Report Simple Verification Technique for Complex Java Bytecode Subroutines of December 2001, revised May 2002. Supersedes Kestrel Institute Technical Report Java Bytecode Subroutines Demistified, referenced in other papers as forthcoming.} 
Checking Access to Protected Members in the Java Virtual Machine
June 2004
6th ECOOP Workshop on Formal Techniques for Javalike Programs (FTfJP)
{Detailed analysis of the requirements on protected member access in the Java Virtual Machine and how to check them. Examples of incorrect checking in Sun’s Java 2 SDK version 1.4 are in [15]. Supersedes Kestrel Institute Technical Report Treatment of Protected Members in Java Bytecode Verification, referenced in other papers as forthcoming.} 
Toward Automatic Generation of Provably Correct Java Card Applets
July 2003
5th ECOOP Workshop on Formal Techniques for Javalike Programs (FTfJP)
{Description of an approach to automatically generate provably correct Java Card applets from highlevel specifications, with details on the code generation backend. Less recent descriptions are in [24, 21]. Also in 4th NSA Conference on High Confidence Software and Systems (HCSS), April 2004.} 
Code Generation for HighAssurance Java Card Applets
April 2003
3rd NSA Conference on High Confidence Software and Systems (HCSS), pages 8593
{Description of the backend code generation component of the approach to automatic applet generation described in [24]. A more recent description is in [20].} 
Improving the Official Specification of Java Bytecode Verification
February 2003
Concurrency and Computation: Practice and Experience, Volume 15, Issue 2, pages 155179
{A comprehensive analysis of Sun’s official specification of Java bytecode verification along with concrete suggestions for improvement. A prelimilinary version is [27].} 
Simple Verification Technique for Complex Java Bytecode Subroutines
June 2002
4th ECOOP Workshop on Formal Techniques for Javalike Programs (FTfJP)
{Overview of the technique defined in [18].} 
An Approach to the Generation of HighAssurance Java Card Applets
March 2002
2nd NSA Conference on High Confidence Software and Systems (HCSS), pages 6977
{Description of an approach to automatically generate provably correct Java Card applets from highlevel specifications. The backend code generation component of the approach is described in [21]. A more recent description is in [20].} 
Type Safety in the JVM: Some Problems in Java 2 SDK 1.2 and Proposed Solutions
(with Allen Goldberg)
November 2001
Concurrency and Computation: Practice and Experience, Volume 13, Issue 13, pages 11531171
{Description of subtle bugs in the Java bytecode verifier of Sun’s Java 2 SDK version 1.2, along with proposed solutions. An overview is in [29]. Supersedes Kestrel Institute Technical Report Type Safety in the JVM: Some Problems in JDK 1.2.2 and Proposed Solutions of April 2000.} 
The Control Layer in Open Mechanized Reasoning Systems: Annotations and Tactics
(with Alessandro Armando, Fausto Giunchiglia, and Silvio Ranise)
October 2001
Journal of Symbolic Computation, Volume 32, Issue 4, pages 305332
{Definition of an extension of the formalism defined in [32] with parameterization; specification of constraint contextual rewriting using the formalism. Overviews of the project within which this work was performed are in [36, 35].} 
Improving the Official Specification of Java Bytecode Verification
June 2001
3rd ECOOP Workshop on Formal Techniques for Java Programs (FTfJP)
{Preliminary version of [22].} 
A Formal Specification of Java Class Loading
(with Allen Goldberg and Zhenyu Qian)
October 2000
15th ACM Conference on ObjectOriented Programming, Systems, Languages, and Applications (OOPSLA), ACM SIGPLAN Notices, Volume 35, Number 10, pages 325336
{Overview of the formalization in [30], enriched with examples and intuitive explanations.} 
Type Safety in the JVM: Some Problems in JDK 1.2.2 and Proposed Solutions
(with Allen Goldberg)
June 2000
2nd ECOOP Workshop on Formal Techniques for Java Programs (FTfJP)
{Overview of the bugs and solutions described in [25].} 
A Formal Specification of Java Class Loading
(with Allen Goldberg and Zhenyu Qian)
April 2000, revised July 2000
Technical Report, Kestrel Institute
{Formalization of Java class loading, including an improvement over Sun’s design that allows lazier loading. An overview of the formalization, enriched with examples and intuitive explanations, is in [28].} 
Composing and Controlling Search in Reasoning Theories Using Mappings
(with Fausto Giunchiglia, José Meseguer, and Carolyn Talcott)
March 2000
3rd Workshop on Frontiers of Combining Systems (FroCoS) Lecture Notes in Artificial Intelligence (LNAI), Number 1794, pages 200216
{Definition of an elaboration of a significant subcase of the formalisms presented in [44] and summarized in [46], where sequents and annotations are built out of equational theories and are related via annotationremoval mappings, and where (annotated) sequents and rules can be nested and composed; specification of the toplevel component of the NQTHM theorem prover using the formalism. An extension of (a subset of) this formalism is defined in [32]; overviews of the project within which this work was performed are in [36, 35].} 
The Control Component of Open Mechanized Reasoning Systems
(with Alessandro Armando and Fausto Giunchiglia)
July 1999
Calculemus'99 Workshop: Systems for Integrated Computation and Deduction, Electronic Notes in Theoretical Computer Science, Volume 23, Issue 3, pages 322339
{Definition of an extension of (a subset of) the formalism defined in [31] with tactics and tactic rules; specification of the toplevel component of the NQTHM theorem prover using the formalism. An extension of this formalism is defined in [26]; overviews of the project within which this work was performed are in [36, 35].} 
Towards a ProvablyCorrect Implementation of the JVM Bytecode Verifier
(with Allen Goldberg and Zhenyu Qian)
October 1998
OOPSLA'98 Workshop on Formal Underpinnings of Java (FUJ)
{Preliminary report on the formal synthesis of a Java bytecode verifier using Kestrel’s Specware system. Also in DARPA Information Survivability Conference and Exposition (DISCEX), Volume 2, pages 403410, January 2000. Also in 1st NSA Conference on High Confidence Software and Systems (HCSS), March 2001.} 
An Architecture for Emotional Agents
(with Antonio Camurri)
October 1998
IEEE Multimedia, Volume 5, Issue 4, pages 2433
{Description of an architecture for agents where an emotional component interacts with rational, reactive, input, and output components; overview of an application of the architecture to the robotic agent of a permanent exhibition. An early version is [41].} 
The OMRS Project: State of the Art
(with Piergiorgio Bertoli and Fausto Giunchiglia)
September 1998
2nd Workshop on Rewriting Logic and Its Applications (WRLA), Volume 15 of Electronic Notes in Theoretical Computer Science, pages 127146
{Overview of the accomplishments and future plans of the Open Mechanized Reasoning Systems (OMRS) project (as of 1998), whose goal is the definition of a formalism to specify and integrate theorem provers. A less detailed overview is in [36]; work performed within this project is described in [46, 44, 32, 31, 26].} 
Open Mechanized Reasoning Systems: A Preliminary Report
(with Alessandro Armando, Piergiorgio Bertoli, Fausto Giunchiglia, José Meseguer, Silvio Ranise, and Carolyn Talcott)
July 1998
CADE15 Workshop on Integration of Deduction Systems (IDS)
{Overview of the accomplishments of the Open Mechanized Reasoning Systems (OMRS) project (as of 1998), whose goal is the definition of a formalism to specify and integrate theorem provers; brief description of two case studies. A more detailed overview is in [35]; work performed within this project is described in [46, 44, 32, 31, 26].} 
Specification of an Executor of Extended Simple Colored Petri Nets
(with Antonio Camurri)
December 1997
Technical Report, Dept. of Informatics, Systems, and Telecommunications (DIST), University of Genoa, Italy
{Formal specification of an executor of the class of highlevel Petri nets defined in [38]. A hybrid architecture for plant simulation that includes this executor is described in [43].} 
Extended Simple Colored Petri Nets
(with Antonio Camurri)
December 1997
Technical Report, Dept. of Informatics, Systems, and Telecommunications (DIST), University of Genoa, Italy
{Extension of the highlevel Petri nets defined in [39]: tokens may include colors from a builtin type for real numbers; stochastic waiting times for tokens are associated to places; and the net has a control interface through which it can be externally supervised. An informal description is in [42] and an executor is formally specified in [37].} 
Simple Colored Petri Nets
(with Antonio Camurri)
November 1997
Technical Report, Dept. of Informatics, Systems, and Telecommunications (DIST), University of Genoa, Italy
{Definition of highlevel Petri nets embodying a tradeoff between the simplicity of (uncolored) Petri nets and the convenience of Colored Petri nets: tokens are tuples of colors from enumerative types that can be structured in hierarchies. An extension is defined in [38].} 
Towards Kansei Evaluation of Movement and Gesture in Music/Dance Interactive Multimodal Environments
(with Antonio Camurri, Roberto Chiarvetto, Massimiliano Di Stefano, Claudia Liconte, Alberto Massari, Claudio Massucco, Daniela Murta, Giuliano Palmieri, Riccardo Rossi, Alessandro Stroscio, and Riccardo Trocca)
October 1997
AIMI Workshop on Kansei: The Technology of Emotion, pages 7478
{Overview of projects at the Laboratory of Musical Informatics (University of Genoa, Italy) focused on movement and gesture analysis as well as communication from machines (e.g. robots) to humans.} 
An Architecture for Multimodal Environment Agents
(with Antonio Camurri, Paolo Coletta, and Claudio Massucco)
October 1997
AIMI Workshop on Kansei: The Technology of Emotion, pages 4853
{Early version of [34].} 
Extended Simple Colored Petri Nets: A Tool for Plant Simulation
(with Antonio Camurri)
October 1997
1997 IEEE Conference on Systems, Man and Cybernetics (SMC), Volume 3, pages 29092914
{Informal description of the highlevel Petri nets formally defined in [38].} 
A Petri Netbased Architecture for Plant Simulation
(with Antonio Camurri)
September 1997
6th IEEE Conference on Emerging Technologies and Factory Automation (ETFA), pages 397402
{Description of an architecture for plant simulation, consisting of a rulebased expert system supervising the executor of highlevel Petri nets specified in [37]; model of a realworld plant using the architecture.} 
A Logic Level Specification of the NQTHM Simplification Process
(with Fausto Giunchiglia, Paolo Pecchiari, and Carolyn Talcott)
July 1997
Technical Report 970048, Dept. of Informatics, Systems, and Telecommunications (DIST), University of Genoa, Italy; Technical Report 970607, IRST, Istituto Trentino di Cultura (ITC), Trento, Italy
{Presentation of a (previously defined) formalism to specify logics of theorem provers by means of generalized sequents, rules, and constraints; specification of a large component of the NQTHM theorem prover using the formalism. An elaboration of a significant subcase of this formalism is defined in [31]; a formalism to specify control strategies of theorem provers, based on this formalism, is summarized in [46]; overviews of the project within which this work was performed are in [36, 35].} 
A Formalism for the Synthesis of Efficient Controllers for Discrete Event Systems
(with Antonio Camurri)
November 1996
5th IEEE Conference on Emerging Technologies and Factory Automation (ETFA), Volume 1, pages 348354
{Overview of a framework to build controllers of discrete event systems (e.g. Petri nets) that recompute, after state changes, only the control directives that depend on state components that have changed.} 
A Formalism for the Control Component of OMRS: NQTHM as a Case Study
May 1996
1st Workshop on Abstraction, Analogy and Metareasoning (AAM)
{Short summary of my thesis work: formalism to specify control strategies of theorem provers by enriching logical inference rules with control annotations and by using tactics and tacticals to construct proofs with the annotated rules; specification of a substantial portion of the NQTHM theorem prover using the formalism. Elaborations of a significant subcase of this formalism are defined in [32, 31, 26]; a formalism to specify logics of theorem provers, on which this formalism is based, is described in [44]; overviews of the project within which this work was performed are in [36, 35].}