[Two kestrels flying]

Home : Research Staff : Alessandro Coglio
 

Home

About Kestrel

Research Staff

Current Projects

Project Archive

Publications

Technology Transfer

Career Opportunities

Contact Kestrel

Alessandro Coglio

Principal Scientist

Kestrel Institute
3260 Hillview Avenue, Palo Alto, CA 94304, USA
Tel: +1-650-493-6871
Fax: +1-650-424-1807
Email: coglio@K.E, where K=kestrel and E=edu

I've been with Kestrel Institute since 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 Manager since 2007. My technical work at Kestrel (Institute and Technology LLC) includes:

  • formal specification and analysis of the type safety mechanisms of the Java Virtual Machine (see [14, 19, 20, 21, 22, 24, 26, 27, 30, 31, 32, 34] and this page);
  • automatic generation of provably correct Java Card applets from higher-level specifications written in a domain-specific language for smart cards (see [25, 28, 29, 33] and this page);
  • contributions to the development of the Specware system:
    • formal definition of the logic of the system (an extension of classical higher-order logic with polymorphism and predicate subtyping);
    • implementation of a proof checker for that logic;
    • design of various mechanisms for composition and refinement;
    • formally defined translation of functional programs to object-oriented programs;
    • development of several libraries;
  • use of the Specware system to:
    • specify and refine to code a complete Java bytecode verifier (see [14] and this page);
    • specify and refine to code a complete Java Card Runtime Environment (see this page);
    • specify and refine to code runtime monitors that provably enforce information flow policies in Java Card Runtime Environments (see this page);
    • specify the memory model of Real-Time Java (see this page);
    • specify and refine to code an embedded software controller for access to a secure enclave via smart card and biometric authentication;
  • general ideas about formal software synthesis (see [15, 17, 33, 35]).

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:

  • development of a formalism to specify control strategies of theorem provers and its application to the NQTHM theorem prover (see [1, 3, 11, 12, 16, 18, 23]) (this was also the topic of my Master thesis);
  • formalization of new classes of high-level Petri nets, implementation 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 (see [2, 4, 5, 8, 9, 10]);
  • development of an architecture for emotional agents (see [6, 7, 13]).

I received a Master-equivalent degree in Informatics Engineering from University of Genoa in 1996. My thesis was in collaboration with ITC-IRST (Trento, Italy) and Stanford University (Palo Alto, California), where I spent a couple of months just after graduating.

During my middle- and high-school years, one of my pastimes was programming videogames (in Assembly) on the glorious Commodore 64 first, then the also-glorious Commodore Amiga. At the university, as a self-assigned course project, I designed and implemented a graphical generator of hypertextual adventure games in Plus (a HyperCard-like system for Windows). Currently, I am investigating formal synthesis of videogames (really).

In case it wasn't clear already, I'm from Italy, more precisely Genoa.

Publications

  1. A Formalism for the Control Component of OMRS: NQTHM as a Case Study
    1st Workshop on Abstraction, Analogy and Metareasoning
    May 1996
    [PS] [BibTeX]
    {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 [16, 18, 23]; a formalism to specify logics of theorem provers, on which this formalism is based, is described in [3]; overviews of the project within which this work was performed are in [11, 12].}

  2. A Formalism for the Synthesis of Efficient Controllers for Discrete Event Systems
    (with Antonio Camurri)
    5th IEEE Conference on Emerging Technologies and Factory Automation (ETFA'96), volume 1, pages 348-354
    November 1996
    [PS] [BibTeX]
    {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.}

  3. A Logic Level Specification of the NQTHM Simplification Process
    (with Fausto Giunchiglia, Paolo Pecchiari, and Carolyn Talcott)
    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
    July 1997
    [PS] [BibTeX]
    {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 [18]; a formalism to specify control strategies of theorem provers, based on this formalism, is summarized in [1]; overviews of the project within which this work was performed are in [11, 12].}

  4. A Petri Net-based Architecture for Plant Simulation
    (with Antonio Camurri)
    6th IEEE Conference on Emerging Technologies and Factory Automation (ETFA'97), pages 397-402
    September 1997
    [PS] [BibTeX]
    {Description of an architecture for plant simulation, consisting of a rule-based expert system supervising the executor of high-level Petri nets specified in [10]; model of a real-world plant using the architecture.}

  5. Extended Simple Colored Petri Nets: A Tool for Plant Simulation
    (with Antonio Camurri)
    1997 IEEE Conference on Systems, Man and Cybernetics (SMC'97), volume 3, pages 2909-2914
    October 1997
    [PS] [BibTeX]
    {Informal description of the high-level Petri nets formally defined in [9].}

  6. An Architecture for Multimodal Environment Agents
    (with Antonio Camurri, Paolo Coletta, and Claudio Massucco)
    AIMI Workshop on Kansei: The Technology of Emotion, pages 48-53
    October 1997
    [PS] [BibTeX]
    {Early version of [13].}

  7. 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)
    AIMI Workshop on Kansei: The Technology of Emotion, pages 74-78
    October 1997
    [PS] [BibTeX]
    {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.}

  8. Simple Colored Petri Nets
    (with Antonio Camurri)
    Technical Report, Dept. of Informatics, Systems, and Telecommunications (DIST), University of Genoa, Italy
    November 1997
    [PS] [BibTeX]
    {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 [9].}

  9. Extended Simple Colored Petri Nets
    (with Antonio Camurri)
    Technical Report, Dept. of Informatics, Systems, and Telecommunications (DIST), University of Genoa, Italy
    December 1997
    [PS] [BibTeX]
    {Extension of the high-level Petri nets defined in [8]: 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 [5] and an executor is formally specified in [10].}

  10. Specification of an Executor of Extended Simple Colored Petri Nets
    (with Antonio Camurri)
    Technical Report, Dept. of Informatics, Systems, and Telecommunications (DIST), University of Genoa, Italy
    December 1997
    [PS] [BibTeX]
    {Formal specification of an executor of the class of high-level Petri nets defined in [9]. A hybrid architecture for plant simulation that includes this executor is described in [4].}

  11. Open Mechanized Reasoning Systems: A Preliminary Report
    (with Alessandro Armando, Piergiorgio Bertoli, Fausto Giunchiglia, José Meseguer, Silvio Ranise, and Carolyn Talcott)
    CADE-15 Workshop on Integration of Deduction Systems
    July 1998
    [PS] [BibTeX]
    {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 [12]; work performed within this project is described in [1, 3, 16, 18, 23].}

  12. The OMRS Project: State of the Art
    (with Piergiorgio Bertoli and Fausto Giunchiglia)
    2nd Workshop on Rewriting Logic and Its Applications (WRLA'98), volume 15 of Electronic Notes in Theoretical Computer Science, Elsevier Science Publishers
    September 1998
    [PS] [BibTeX]
    {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 [11]; work performed within this project is described in [1, 3, 16, 18, 23].}

  13. An Architecture for Emotional Agents
    (with Antonio Camurri)
    IEEE Multimedia, 5(4):24-33
    October 1998
    [PDF] [BibTeX]
    {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 [6].}

  14. Towards a Provably-Correct Implementation of the JVM Bytecode Verifier
    (with Allen Goldberg and Zhenyu Qian)
    OOPSLA'98 Workshop on Formal Underpinnings of Java
    October 1998
    [PS] [PDF] [BibTeX]
    {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'00), volume 2, pages 403-410, IEEE Computer Society Press, January 2000. Also in 1st NSA Conference on High Confidence Software and Systems, March 2001.}

  15. Components as Refinements
    Workshop on Software Behavior Description
    December 1998
    [PS] [PDF] [BibTeX]
    {Position paper envisioning formal development by composition and refinement as a key supporting technology for truly re-usable software components.}

  16. The Control Component of Open Mechanized Reasoning Systems
    (with Alessandro Armando and Fausto Giunchiglia)
    Calculemus'99 Workshop: Systems for Integrated Computation and Deduction, volume 23, issue 3 of Electronic Notes in Theoretical Computer Science, Elsevier Science Publishers
    July 1999
    [PS] [BibTeX]
    {Definition of an extension of (a subset of) the formalism defined in [18] 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 [23]; overviews of the project within which this work was performed are in [11, 12].}

  17. Automated Formal Development by Composition and Refinement: A Key Technology for Software Development in the Post-PC World
    Workshop on Software Development for the Post-PC World
    December 1999
    [PS] [PDF] [BibTeX]
    {Short position paper arguing for formal development by composition and refinement as a key supporting technology for the realization of highly coordinated, ubiquitous computing systems.}

  18. Composing and Controlling Search in Reasoning Theories Using Mappings
    (with Fausto Giunchiglia, José Meseguer, and Carolyn Talcott)
    3rd Workshop on Frontiers of Combining Systems (FroCoS'00), number 1794 in Lecture Notes in Artificial Intelligence (LNAI), pages 200-216, Springer-Verlag
    March 2000
    [PS] [BibTeX]
    {Definition of an elaboration of a significant subcase of the formalisms presented in [3] and summarized in [1], 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 [16]; overviews of the project within which this work was performed are in [11, 12].}

  19. A Formal Specification of Java Class Loading
    (with Allen Goldberg and Zhenyu Qian)
    Technical Report, Kestrel Institute
    April 2000, revised July 2000
    [PS] [PDF] [BibTeX]
    {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 [21].}

  20. Type Safety in the JVM: Some Problems in JDK 1.2.2 and Proposed Solutions
    (with Allen Goldberg)
    2nd ECOOP Workshop on Formal Techniques for Java Programs
    June 2000
    [PS] [PDF] [BibTeX]
    {Overview of the bugs and solutions described in [24].}

  21. A Formal Specification of Java Class Loading
    (with Allen Goldberg and Zhenyu Qian)
    15th ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'00), volume 35, number 10 of ACM SIGPLAN Notices, pages 325-336
    October 2000
    [PS] [PDF] [BibTeX]
    {Overview of the formalization in [19], enriched with examples and intuitive explanations.}

  22. Improving the Official Specification of Java Bytecode Verification
    3rd ECOOP Workshop on Formal Techniques for Java Programs
    June 2001
    [PS] [PDF] [BibTeX]
    {Preliminary version of [27].}

  23. The Control Layer in Open Mechanized Reasoning Systems: Annotations and Tactics
    (with Alessandro Armando, Fausto Giunchiglia, and Silvio Ranise)
    Journal of Symbolic Computation, 32(4):305-332
    October 2001
    [PS] [BibTeX]
    {Definition of an extension of the formalism defined in [16] with parameterization; specification of constraint contextual rewriting using the formalism. Overviews of the project within which this work was performed are in [11, 12].}

  24. Type Safety in the JVM: Some Problems in Java 2 SDK 1.2 and Proposed Solutions
    (with Allen Goldberg)
    Concurrency and Computation: Practice and Experience, 13(13):1153-1171
    November 2001
    [PDF] [BibTeX]
    {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 [20]. Supersedes Kestrel Institute Technical Report Type Safety in the JVM: Some Problems in JDK 1.2.2 and Proposed Solutions of April 2000. Source code, compilation instructions, and class files to demonstrate the bugs are available here.}

  25. An Approach to the Generation of High-Assurance Java Card Applets
    2nd NSA Conference on High Confidence Software and Systems, pages 69-77
    March 2002
    [PS] [PDF] [BibTeX]
    {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 [28]. A more recent description is in [29].}

  26. Simple Verification Technique for Complex Java Bytecode Subroutines
    4th ECOOP Workshop on Formal Techniques for Java-like Programs
    June 2002
    [PS] [PDF] [BibTeX]
    {Overview of the technique defined in [31].}

  27. Improving the Official Specification of Java Bytecode Verification
    Concurrency and Computation: Practice and Experience, 15(2):155-179
    February 2003
    [PDF] [BibTeX]
    {A comprehensive analysis of Sun's official specification of Java bytecode verification along with concrete suggestions for improvement. A prelimilinary version is [22]}

  28. Code Generation for High-Assurance Java Card Applets
    3rd NSA Conference on High Confidence Software and Systems, pages 85-93
    April 2003
    [PS] [PDF] [BibTeX]
    {Description of the back-end code generation component of the approach to automatic applet generation described in [25]. A more recent description is in [29].}

  29. Toward Automatic Generation of Provably Correct Java Card Applets
    5th ECOOP Workshop on Formal Techniques for Java-like Programs
    July 2003
    [PS] [PDF] [BibTeX]
    {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 [25, 28]. Also in 4th NSA Conference on High Confidence Software and Systems, April 2004.}

  30. Checking Access to Protected Members in the Java Virtual Machine
    6th ECOOP Workshop on Formal Techniques for Java-like Programs
    June 2004
    [PS] [PDF] [BibTeX]
    {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 [34]. Supersedes Kestrel Institute Technical Report Treatment of Protected Members in Java Bytecode Verification, referenced in other papers as forthcoming.}

  31. Simple Verification Technique for Complex Java Bytecode Subroutines
    Concurrency and Computation: Practice and Experience, 16(7):647-670
    June 2004
    [PDF] [BibTeX]
    {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.}

  32. Formal Techniques for Java-Like Programs (FTfJP)
    (with Marieke Huisman, Joseph Kiniry, Peter Müller, and Erik Poll)
    Object-Oriented Technology. ECOOP 2004 Workshop Reader, number 3344 in Lecture Notes in Computer Science (LNCS), pages 76-83, Springer-Verlag
    January 2005
    [PDF] [BibTeX]
    {Report on the workshop.}

  33. A Constructive Approach to Correctness, Exemplified by a Generator for Certified Java Card Applets
    (with Cordell Green)
    IFIP Working Conference on Verified Software: Tools, Techniques, and Experiments (VSTTE), number 4171 in Lecture Notes in Computer Science (LNCS), pages 57-63, Springer
    October 2005
    [PS] [PDF] [BibTeX]
    {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.}

  34. Checking Access to Protected Members in the Java Virtual Machine
    Journal of Object Technology
    October 2005
    [PDF] [BibTeX]
    {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 [30]. Supersedes Kestrel Institute Technical Report Checking Access to Protected Members in the Java Virtual Machine of February 2004.}

  35. 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)
    5th International Conference on Generative Programming and Component Engineering (GPCE'06)
    October 2006
    [PDF] [BibTeX]
    {Roadmap for research to further the goal of verified software.}

Some of the publications above happen to be copyrighted by the indicated publishers. So, the usual legalese applies here: namely, personal use is allowed, but not re-publishing, etc.

 

- Back to Top -


- Home - About Kestrel - Research Staff - Current Projects - Project Archive -
- Publications - Technology Transfer - Career Opportunities - Contact Kestrel -