Home : Project Archive : CPR
 

Composability, Provability and Reusability for Survivable Systems

Allen Goldberg, Principal Investigator
Zhenyu Qian
Alessandro Coglio
Richard Waldinger

Papers related to the project:

• Zhenyu Qian. Constraint-Based Specification and Dataflow Analysis for Java(TM) Bytecode Verification. abstract, postscript
• Alessandro Coglio, Allen Goldberg, and Zhenyu Qian. Towards a Provably-Correct Implementation of the JVM Bytecode Verifier. submitted for publication. 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, postscript

We have included a slide show that describes in detail the work on the Java Bytecode Verifier

We describe our objective and approach to the project.

- Back to Top -

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