# Alessandro Coglio

## Contact

coglio@K.E, where K=kestrel and E=edu

GitHub: acoglio

## Bio

I'm a Principal Scientist at Kestrel Institute, which I joined in 1998. I'm also a Co-founder of, Board Director of, and Principal Software Engineer at Kestrel Technology LLC (a spin-off of Kestrel Institute). My current and past work at Kestrel includes:

- Development of techniques for program specification, refinement, transformation, synthesis, and verification [9, 6, 3, 2, 14, 12]. Implementation in ACL2 [6, 3]. Application to numerous examples in a variety of domains. Also see the APT, Hyperproperties, DerivationMiner, and Specware project pages.
- Formalization of the syntax and semantics of ABNF (Augmented Backus-Naur Form), development of a verified parser of ABNF grammars, and development of operations on ABNF grammars, using ACL2 [4].
- Formal specification of Bitcoin and Ethereum in ACL2. Also see the ACL2 Ethereum project page.
- Extension to 32-bit mode of an open-source formal model in ACL2 of the x86 Instruction Set Architecture [1].
- Formal specification of a resolution-based 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 [31, 26, 28, 27, 23, 25, 20, 21, 16, 17, 13, 15] (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 higher-level specifications written in a domain-specific language for smart cards [22, 19, 18, 14]. 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 multi-domain multi-level security, and their application to an information architecture for distributed embedded systems such as fractionated satellites [11, 10, 8]. Also see the F6 project page.
- Formal verification of Android apps using ACL2 [7]. 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 [5]. Also see the VIBRANCE project page.
- Contributions to the Isabelle library and Archive of Formal Proofs [9].
- Contributions to the ACL2 library [4, 6, 3, 1, 2].

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 [44, 42, 34, 33, 30, 29, 24] (this was also the topic of my thesis).
- Formalization of new classes of high-level 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 [43, 41, 40, 37, 36, 35].
- Architecture for emotional agents [39, 32, 38].

I received a degree in Informatics Engineering from University of Genoa in 1996. My thesis was in collaboration with ITC-IRST (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 high-school years, I designed and implemented some video games in Assembly on the glorious Commodore 64 first, then on the also-glorious Commodore Amiga. During my university years, I designed and implemented a graphical generator of hypertextual adventure games in Plus (a HyperCard-like 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

**Adding 32-bit 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 (ACL2-2018)*

{Description of how the x86 formal model in ACL2 was extended from 64-bit mode to 32-bit 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 (ACL2-2018)*

{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 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 (ACL2-2017)*

{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.}**ABNF in ACL2**

April 2017

*Technical Report, Kestrel Institute*

{Description of (i) a formalization of the syntax and semantics of the ABNF (Augmented Backus-Naur Form) notation and (ii) a verified parser that turns ABNF grammar text into a formal representation usable in declarative specifications of parsers of ABNF-specified languages. A slightly improved version of this technical report will appear as a paper in the VSTTE 2018 post-conference proceedings; that paper will supersede this technical report.}**AutoRand: Automatic Keyword Randomization to Prevent Injection Attacks**

(with Jeff Perkins, Jordan Eikenberry, Daniel Willenson, Stelios Sidiroglou-Douskos, 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.}**Second-Order Functions and Theorems in ACL2**

October 2015

*13th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2015)*, pages 17-33

{Description of SOFT (= Second-Order Functions and Theorems), an ACL2 library to mimic second-order functions and theorems in the first-order logic of ACL2; example of use of SOFT in the shallow pop-refinement approach to program refinement. Shallow pop-refinement is a form of pop-refinement [9] 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 Working Conference on Verified Software: Tools, Techniques, and Experiments (VSTTE)*

{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 (SMC-IT)*, pages 67-74

{More detailed description of the secure communications mechanisms in the architecture overviewed in [11] and [10].}**Pop-Refinement**

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*Pop-Refinement*of November 2013. Supersedes Kestrel Institute Technical Report*A Simple Example of Pop-Refinement in Isabelle/HOL*of November 2013. Supersedes Kestrel Institute Technical Report*A Simple Example of Pop-Refinement and Hyperproperties in Isabelle/HOL*of January 2014.}**DREMS: A Model-Driven 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 62-69

{Overview of a multi-level secure, fault-tolerant information architecture, and associated model-based development tools, for embedded systems. An earlier version of this architecure, tailored to fractionated satellites, is described in [11].}**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 1-20

{Overview of a multi-level secure, fault-tolerant information architecture, and associated model-based 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 [10].}**Roadmap for Enhanced Languages and Methods to Aid Verification**

(with Gary Leavens, Jean-Raymond Abrial, Don Batory, Michael Butler, Kathi Fisler, Eric Hehner, Cliff Jones, Dale Miller, Simon Peyton-Jones, Murali Sitaraman, Doug Smith, and Aaron Stump)

October 2006

*5th International Conference on Generative Programming and Component Engineering (GPCE)*, pages 221-236

{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 55-76

{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 [17]. 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

*IFIP Working Conference on Verified Software: Tools, Techniques, and Experiments (VSTTE)*,*Lecture Notes in Computer Science (LNCS)*, Number 4171, pages 57-63

{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 Java-Like Programs (FTfJP)**

(with Marieke Huisman, Joseph Kiniry, Peter Müller, and Erik Poll)

January 2005

*Object-Oriented Technology. ECOOP 2004 Workshop Reader*,*Lecture Notes in Computer Science (LNCS)*, Number 3344, pages 76-83

{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 647-670

{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 [21]. 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 Java-like 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 [13]. 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 Java-like Programs (FTfJP)*

{Description of an approach to automatically generate provably correct Java Card applets from high-level specifications, with details on the code generation back-end. Less recent descriptions are in [22, 19]. Also in*4th NSA Conference on High Confidence Software and Systems (HCSS)*, April 2004.}**Code Generation for High-Assurance Java Card Applets**

April 2003

*3rd NSA Conference on High Confidence Software and Systems (HCSS)*, pages 85-93

{Description of the back-end code generation component of the approach to automatic applet generation described in [22]. A more recent description is in [18].}**Improving the Official Specification of Java Bytecode Verification**

February 2003

*Concurrency and Computation: Practice and Experience*, Volume 15, Issue 2, pages 155-179

{A comprehensive analysis of Sun's official specification of Java bytecode verification along with concrete suggestions for improvement. A prelimilinary version is [25].}**Simple Verification Technique for Complex Java Bytecode Subroutines**

June 2002

*4th ECOOP Workshop on Formal Techniques for Java-like Programs (FTfJP)*

{Overview of the technique defined in [16].}**An Approach to the Generation of High-Assurance Java Card Applets**

March 2002

*2nd NSA Conference on High Confidence Software and Systems (HCSS)*, pages 69-77

{Description of an approach to automatically generate provably correct Java Card applets from high-level specifications. The back-end code generation component of the approach is described in [19]. A more recent description is in [18].}**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 1153-1171

{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 [27]. 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 305-332

{Definition of an extension of the formalism defined in [30] with parameterization; specification of constraint contextual rewriting using the formalism. Overviews of the project within which this work was performed are in [34, 33].}**Improving the Official Specification of Java Bytecode Verification**

June 2001

*3rd ECOOP Workshop on Formal Techniques for Java Programs (FTfJP)*

{Preliminary version of [20].}**A Formal Specification of Java Class Loading**

(with Allen Goldberg and Zhenyu Qian)

October 2000

*15th ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA)*,*ACM SIGPLAN Notices*, Volume 35, Number 10, pages 325-336

{Overview of the formalization in [28], 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 [23].}**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 [26].}**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 200-216

{Definition of an elaboration of a significant subcase of the formalisms presented in [42] and summarized in [44], where sequents and annotations are built out of equational theories and are related via annotation-removal mappings, and where (annotated) sequents and rules can be nested and composed; specification of the top-level component of the NQTHM theorem prover using the formalism. An extension of (a subset of) this formalism is defined in [30]; overviews of the project within which this work was performed are in [34, 33].}**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 322-339

{Definition of an extension of (a subset of) the formalism defined in [29] with tactics and tactic rules; specification of the top-level component of the NQTHM theorem prover using the formalism. An extension of this formalism is defined in [24]; overviews of the project within which this work was performed are in [34, 33].}**Towards a Provably-Correct 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 403-410, 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 24-33

{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 [39].}**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 127-146

{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 [34]; work performed within this project is described in [44, 42, 30, 29, 24].}**Open Mechanized Reasoning Systems: A Preliminary Report**

(with Alessandro Armando, Piergiorgio Bertoli, Fausto Giunchiglia, José Meseguer, Silvio Ranise, and Carolyn Talcott)

July 1998

*CADE-15 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 [33]; work performed within this project is described in [44, 42, 30, 29, 24].}**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 high-level Petri nets defined in [36]. A hybrid architecture for plant simulation that includes this executor is described in [41].}**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 high-level Petri nets defined in [37]: tokens may include colors from a built-in 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 [40] and an executor is formally specified in [35].}**Simple Colored Petri Nets**

(with Antonio Camurri)

November 1997

Technical Report, Dept. of Informatics, Systems, and Telecommunications (DIST), University of Genoa, Italy

{Definition of high-level Petri nets embodying a trade-off 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 [36].}**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 74-78

{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 48-53

{Early version of [32].}**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 2909-2914

{Informal description of the high-level Petri nets formally defined in [36].}**A Petri Net-based Architecture for Plant Simulation**

(with Antonio Camurri)

September 1997

*6th IEEE Conference on Emerging Technologies and Factory Automation (ETFA)*, pages 397-402

{Description of an architecture for plant simulation, consisting of a rule-based expert system supervising the executor of high-level Petri nets specified in [35]; model of a real-world 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 97-0048, Dept. of Informatics, Systems, and Telecommunications (DIST), University of Genoa, Italy; Technical Report 9706-07, 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 [29]; a formalism to specify control strategies of theorem provers, based on this formalism, is summarized in [44]; overviews of the project within which this work was performed are in [34, 33].}**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 348-354

{Overview of a framework to build controllers of discrete event systems (e.g. Petri nets) that re-compute, 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 [30, 29, 24]; a formalism to specify logics of theorem provers, on which this formalism is based, is described in [42]; overviews of the project within which this work was performed are in [34, 33].}