Concurrent Program Refinement Compilers for concurrent programs Linearizability of concurrent objects(libraries) Impl. of software transactional memory stm) Impl of concurrent garbage collectors (Gc) Impl of operating system(OS) kernels Is such a refinement T c s general enough easy to verify?Concurrent Program Refinement • Compilers for concurrent programs • Linearizability of concurrent objects (libraries) • Impl. of software transactional memory (STM) • Impl. of concurrent garbage collectors (GC) • Impl. of operating system (OS) kernels Is such a refinement T  S general enough & easy to verify?