[Kestrel circling]

Home : Project Archive : CPR
 

Home

About Kestrel

Research Staff

Current Projects

Project Archive

Publications

Technology Transfer

Career Opportunities

Contact Kestrel

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 -