Alessandro Coglio

Contact

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

Address/Phone/Fax

Bio

I'm a Principal Scientist at Kestrel Institute, which I joined in 1998. I'm also a Co-founder of Kestrel Technology LLC (a spin-off of Kestrel Institute), where I've been a Computer Scientist between 2001 and 2007, and a Board Director since 2007. 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:

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. AutoRand: Automatic Keyword Randomization to Prevent Injection Attacks
    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 injectable the keywords within the application.}

  2. 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 [5] 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.}

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

  4. 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 [7] and [6].}

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

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

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

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

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

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

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

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

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

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

  15. 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 [18]. A more recent description is in [14].}

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

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

  18. 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 [15]. A more recent description is in [14].}

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

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

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

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

  23. 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 [19].}

  24. 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 [22].}

  25. 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 [38] and summarized in [40], 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 [26]; overviews of the project within which this work was performed are in [30, 29].}

  26. 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 [25] 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 [20]; overviews of the project within which this work was performed are in [30, 29].}

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

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

  29. 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 [30]; work performed within this project is described in [40, 38, 26, 25, 20].}

  30. 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 [29]; work performed within this project is described in [40, 38, 26, 25, 20].}

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

  32. 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 [33]: 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 [36] and an executor is formally specified in [31].}

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

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

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

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

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

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

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

  40. 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 [26, 25, 20]; a formalism to specify logics of theorem provers, on which this formalism is based, is described in [38]; overviews of the project within which this work was performed are in [30, 29].}