Technische Universität München, Department of Computer Science, Chair IV: Software & Systems Engineering, Theorem Proving Group
One main goal of the project is to develop a fully formal foundation of a PCC system. This includes verified components of the trusted code base and soundness of the safety logic. The formalization will make explicit what properties soundness guarantees, and under which assumptions the trusted code base (mainly the vcg) works correctly. The formalization of the receiver side will be generic in safety logic, safety policy, and target machine.
On the code producer side we will analyse existing methods for static analysis of programs and extend them to generate proofs in a suitable safety logic. These proofs must show the correctness of the analysis. The safety policies and analyses we will investigate are arithmetic overflow and ressource constraints (in time and space).
This project is funded by the DFG.
PCC Framework | Defines a generic VCG and requirements that guarantee its soundness. |
Instantiation | Progr. Lang. | Safety Logic | Safety Policy |
SALTypeSafety | SAL (without procedures, pointers) | shallow embedded HOL | Type Safety |
SALOverflowShallow | SAL | shallow embedded HOL | Type Safety, No Overflows |
SALTime | SAL | shallow embedded HOL | Type Safety, No Overflows, Bounded Runtime |
SALMemory | SAL | shallow embedded HOL | Type Safety, No Overflows, Bounded Memory |
SALOverflowDeep | SAL |
deep embedded FOA with HOL inference system |
Type Safety, No Overflows |
JinjaPCC |
Jinja Bytecode (fragment of Java Bytecode) |
deep embedded FOA with OO elements | No Overflows |
PA.zip | Contains the Program Analyzer (required only for the Jinja Theories) Unzip to directory ~/work/PA |
PCCTheories.zip | Contains all PCC Theories Unzip to directory ~/work/PCC/ |
Martin Wildmoser | Last modified: Wed Jan 25 12:37:48 MET 2006 |