Technische Universität München, Department of Computer Science, Chair IV: Software & Systems Engineering, Theorem Proving Group, VeryPCC Project
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. |
|
||||||||
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. |
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. |
Martin Wildmoser | Last modified: Wed Jan 18 12:07:40 MET 2006 |