Technische Universität München, Department of Computer Science, Chair IV: Software & Systems Engineering, Theorem Proving Group, VeryPCC Project

[empty]

PCC Instantiation - Overflow safety for Jinja Bytecode


[empty] In these theories we instantiate our Proof Carrying Code Framework to Jinja Bytecode. Jinja is a formalisation of major parts of Java and its Java Virtual Machine in Isabelle/HOL. The VCG turns Jinja Bytecode into proof obligations (formulae in a first order assertion language) that guarantee that arithmetic operations do not overflow. The safety logic is deeply embedded into Isabelle/HOL, which can be used as prover and proof checker. [empty]

[empty]
Machine Code: Jinja Bytecode
Safety Policy: No overflows
Safety Logic: First Order Arithmetics
[empty] [empty]
[empty]
Form.thy [pdf] The Sytax of formulas and operations on these.
JBC_Semantics.thy [pdf] A formal semantics for Jinja Bytecode.
JBC_SafetyPolicy.thy [pdf] Defines the safety policy: reject arithmetic overflows.
JBC_SafetyLogic.thy [pdf] First order arithmetics enriched with OO specific operators.
JBC_VCG.thy [pdf] Instantiates the VCG.
JBC_SysInv.thy [pdf] Proves system invariants for Jinja.
JBC_wpFcorrect.thy [pdf] Verifies the weakest precondition operator.
JBC_succsFcorrect.thy [pdf] Verifies the control flow function. Every machine transition occurs in the control flow.
JBC_Correctness.thy [pdf] Verifies the correctness of the instantiated VCG. Instantiates PCCFramework/VCG_Correctness.thy.
JBC_succsFprogress.thy [pdf] Verifies the control flow function. Every edge in the control flow indicates a possible machine transition.
JBC_VCG_Completess.thy [pdf] Verifies the completeness of the instantiated VCG. Instantiates PCCFramework/VCG_Completeness.thy.
JBC_Expressiveness.thy [pdf] Verifies the expressiveness requirements. Instantiates locale exprSL from PCCFramework/VCG_Completeness.thy.
VCOpt.thy [pdf] Defines and verifies optimizing formula transformers.
VCGExec.thy [pdf] Generates executable ML code for the VCG.


Examples

EX_MainSumAuto.thy [pdf] A main method which adds the numbers from 1 to N. Annotations are computed automatically via program analysis.
EX_MainSum.thy [pdf] A main method which adds the numbers from 1 to N. We discuss various annotations that prove or fail to prove safety.
EX_Sum.thy [pdf] Creates an object and calls its summation method, which adds the numbers from 1 to N.
[empty]
Martin Wildmoser Last modified: Wed Jan 18 12:07:40 MET 2006