Composability, Provability and Reusability for Survivable Systems

Papers related to the project:

• Zhenyu Qian. Constraint-Based Specification and Dataflow Analysis for Java(TM) Bytecode Verification. abstract, pdf, postscript
• Alessandro Coglio, Allen Goldberg, and Zhenyu Qian. Towards a Provably-Correct Implementation of the JVM Bytecode Verifier. submitted for publication. pdf, postscript
• Allen Goldberg. A Specification of Java Loading and Bytecode Verification. To appear in, Proceedings, 5th ACM Conference on Computer and Communications Security, San Francisco, October 1998. abstract, pdf
• Zhenyu Qian. A Formal Specification of a Large Subset of Java(tm) Virtual Machine Instructions for Objects, Methods and Subroutines. To appear in, Jim Alves-Foss (Ed.), Formal Syntax and Semantics of Java(TM). Springer Verlag LNCS, 1998. abstract, pdf, postscript

We describe our objective and approach to the project.