Regular Meetings: Thursday 07:30-09:30pm   211 Room

if you are a registered user, you can download the slides or documents about  the topic from here

You are Invited!

 Please send email to Yu Guo if you  :

  • are interested in giving a talk;
  • want to suggest a research topic paper , or current event for the group to discuss;
Date Presenter Topic
Nov.18 Ming Fu Reasoning about optmistic concurrency using a program logic for history
Nov.25  Gang Tan GoNative: Safe native code for safe language
Dec.02 Yu Guo Cerified thread scheduler
Dec.09 Wei Hu Survey results of "CoreDet"
Dec.23 Hongjin Liang Quick Study : Logical Relation

Wei Wang


Xi Wang

The rehearse of  thesis proposal


2011.02-2011.07 Semester
Date Presenter Topic
Jan.06 Quanlong Li   Design of channel-based determintic languaged                          
Feb.24 Yiyun Chen The soundness of shape graph logic
Mar.03 Xinyu Feng Some random thoughts on doing research
Mar.10 Quanlong Li The Semantics of Channel-based Deterministic Language
Mar.17 Yang Zhang An operational approach to Relaxed memory models
Mar.24 Yu Guo Invariant of shared resources for cooperative threads
Mar.31 Ming Fu Trace-based Concurrent Separation Logic
Apr.7 Hongjin Liang A Framework for Verifying Concurrent Garbage Collectors
Apr.22 Xi Wang Verification of  Virtual Memory
May.4 ZhaoPeng Li Tool Supports in C Program Verification
Søren Debois
Introduction to Bifraphs & Computation in Bigraphs
May.12 Xinyu Feng Relational Reasoning about Concurrent Program Transformation
May.24 JingJiang Lei An Approach for Verification of Lock-free Algorithms