Alessandro Coglio

Contact
e-mail:
address: Contact page
GitHub: acoglio
LinkedIn: Alessandro Coglio

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:

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 [49, 47, 39, 38, 35, 34, 29] (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 [48, 46, 45, 42, 41, 40].

  • Architecture for emotional agents [44, 37, 43].

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

  1. A Proof-Generating C Code Generator for ACL2 Based on a Shallow Embedding of C in ACL2
    May 2022
    17th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2022)
    {Description of a tool to generate C code from ACL2 code that closely represents the C code; the tool also generates ACL2 proofs of correctness of the C code with respect to the ACL2 code. This tool is design for use in program synthesis with APT.}

  2. A Complex Java Code Generator for ACL2 Based on a Shallow Embedding of ACL2 in Java
    May 2022
    17th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2022)
    {Desciption of a substantial extension of the code generator described in [7], which produces more efficient and idiomatic Java code, by translating the ACL2 code into suitably equivalent Java code.}

  3. Syntheto: A Surface Language for APT and ACL2
    (with Eric McCarthy, Stephen Westfold, Daniel Balasubramanian, Abhishek Dubey, and Gabor Karsai)
    May 2022
    17th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2022)
    {Description of a prototype language that provides a more familiar and accessible interface to APT and ACL2.}

  4. Ethereum's Recursive Length Prefix in ACL2
    May 2020
    16th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2020)
    {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 self-contained. Supersedes Kestrel Institute Technical Report Ethereum’s Recursive Length Prefix in ACL2 of August 2019.}

  5. Isomorphic Data Type Transformations
    (with Stephen Westfold)
    May 2020
    16th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2020)
    {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.}

  6. 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.}

  7. 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 substantial extension of this code generator is described in [2].}

  8. 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 177-195
    {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. Supersedes Kestrel Institute Technical Report ABNF in ACL2 of July 2017.}

  9. 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.}

  10. 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.}

  11. 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 [14] 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.}

  12. 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 183-201
    {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.}

  13. 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 [16] and [15].}

  14. 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.}

  15. 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 [16].}

  16. 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 [15].}

  17. 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.}

  18. 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 [22]. Supersedes Kestrel Institute Technical Report Checking Access to Protected Members in the Java Virtual Machine of February 2004.}

  19. 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 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.}

  20. 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.}

  21. 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 [26]. 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.}

  22. 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 [18]. Supersedes Kestrel Institute Technical Report Treatment of Protected Members in Java Bytecode Verification, referenced in other papers as forthcoming.}

  23. 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 [27, 24]. Also in 4th NSA Conference on High Confidence Software and Systems (HCSS), April 2004.}

  24. 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 [27]. A more recent description is in [23].}

  25. 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 [30].}

  26. 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 [21].}

  27. 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 [24]. A more recent description is in [23].}

  28. 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 [32]. Supersedes Kestrel Institute Technical Report Type Safety in the JVM: Some Problems in JDK 1.2.2 and Proposed Solutions of April 2000.}

  29. 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 [35] with parameterization; specification of constraint contextual rewriting using the formalism. Overviews of the project within which this work was performed are in [39, 38].}

  30. Improving the Official Specification of Java Bytecode Verification
    June 2001
    3rd ECOOP Workshop on Formal Techniques for Java Programs (FTfJP)
    {Preliminary version of [25].}

  31. 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 [33], enriched with examples and intuitive explanations.}

  32. 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 [28].}

  33. 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 [31].}

  34. 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 [47] and summarized in [49], 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 [35]; overviews of the project within which this work was performed are in [39, 38].}

  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 322-339
    {Definition of an extension of (a subset of) the formalism defined in [34] 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 [29]; overviews of the project within which this work was performed are in [39, 38].}

  36. 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.}

  37. 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 [44].}

  38. 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 [39]; work performed within this project is described in [49, 47, 35, 34, 29].}

  39. 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 [38]; work performed within this project is described in [49, 47, 35, 34, 29].}

  40. 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 [41]. A hybrid architecture for plant simulation that includes this executor is described in [46].}

  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 [42]: 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 [45] and an executor is formally specified in [40].}

  42. 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 [41].}

  43. 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.}

  44. 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 [37].}

  45. 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 [41].}

  46. 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 [40]; model of a real-world plant using the architecture.}

  47. 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 [34]; a formalism to specify control strategies of theorem provers, based on this formalism, is summarized in [49]; overviews of the project within which this work was performed are in [39, 38].}

  48. 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.}

  49. 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 [35, 34, 29]; a formalism to specify logics of theorem provers, on which this formalism is based, is described in [47]; overviews of the project within which this work was performed are in [39, 38].}