Concurrent Program Refinement Compilers for concurrent programs Multithreaded S Java programs Correct( Compiler) Compiler VS, T. T= Compilers)=TcS Java bytecodeConcurrent Program Refinement • Compilers for concurrent programs T S Compiler Multithreaded Java programs Java bytecode Correct(Compiler): S, T. T = Compiler(S)  T  S