Motivation Proof-carrying code (PCC) In principle:verify any property on any code Real binaries no loss of efficiency Embedded OS,device drivers... All safety liveness properties... Formal,machine-checkable proofs In reality:only works for sequential code Can concurrent code ever be supported by the PCC framework 2005-9-16 NJPLS@Stevens2005-9-16 NJPLS@Stevens Motivation ◼ Proof-carrying code (PCC) ◼ In principle: verify any property on any code ◼ Real binaries & no loss of efficiency ◼ Embedded OS, device drivers… ◼ All safety & liveness properties… ◼ Formal, machine-checkable proofs ◼ In reality: only works for sequential code Can concurrent code ever be supported by the PCC framework ?