Challenges Challenges for Proof-carrying concur.code -A general framework for concurrent assembly code verification Lack of structures(e.g.cobegin/coend blocks) Specification/proof generation Spec inference,proof assistant,theorem prover ■（ Concurrent assembly code verification No directly applicable logic Traditional Hoare-logic:only sequential code Type Systems:no Concurrent Typed Assembly Language (TAL) 2005-9-16 NJPLS@Stevens2005-9-16 NJPLS@Stevens Challenges ◼ Challenges for Proof-carrying concur. code ◼ A general framework for concurrent assembly code verification ◼ Lack of structures (e.g. cobegin/coend blocks) ◼ Specification/proof generation ◼ Spec inference, proof assistant, theorem prover ◼ Concurrent assembly code verification ◼ No directly applicable logic ◼ Traditional Hoare-logic: only sequential code ◼ Type Systems: no Concurrent Typed Assembly Language (TAL)