Model Checking with PAT

Wednesday, 24th February 2010, 10:00 am (PDCC Meeting Room)
Speaker: Dr Sun Jun (NUS)
Title: Model Checking with PAT

Model checking has emerged as an effective method for system verification. It is finding ways into many domains. In this talk, I will present the project named PAT ( PAT is a framework for developing domain specific model checking facilities, including domain specific modelling language, semantics, abstraction as well as verification algorithms. Within two years, PAT has attracted hundreds of registered users and has been adopted as an educational tool in multiple universities.

Distributed systems are an important application domain of model checking. PAT offers specialized algorithms to deal with parallel execution of system components. For instance, PAT supports verification of distributed systems under a variety of notions of fairness, verification of lineariability of parallel data structures, etc. Previously unknown bugs in recently proposed distributed algorithms have been identified using PAT. In order to verify real-world distributed systems (instead of distributed algorithms), PAT is recently extended with support for real-time as well as probabilistic system behaviours.


Dr. Jun Sun received Bachelor and PhD degree in School of Computing, National University of Singapore (NUS) in 2002 and 2006. Since 2006, he was named a Lee Kuan Yew Postdoctoral fellow at Department of Computer Science, NUS. His research interests are mainly in formal system specification, verification and synthesis. Recently, he founded the PAT framework for model checking. He has more than 40 publications, including articles in IEEE Trans. on SE and ACM Trans. on SE as well as papers in CAV, ICSE and FM. More details about his research and background can be found at: