Title: Pervasive Model Checking

Speaker: Dr LIU Yang (Nanyang Technological University)

Time: 15:00, Wednesday, September 19th, 2012

Venue: Room 334, 3rd Floor, Building 5#, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences

Abstract:

Model checking is emerging as an effective software verification method with wide applications. However, still there are a lot research challenges in model checking techniques and in applying model checking techniques. To address these challenges, this talk presents our research contributions in the system modeling, efficient model checking algorithms development and effective reduction techniques. More important, we introduce a process analysis toolkit (PAT, www.patroot.com), which is a self-contained verification framework for specification, simulation and verification of concurrent, real-time and probabilistic systems. PAT architecture provides extensibility in many possible aspects: modeling languages, model checking algorithms, reduction techniques and so on. Various model checkers have been developed under this new architecture in short time. Since PAT is released 5 years ago, it has attracted 2000+ registered users world wide. Our vision is to achieve pervasive model checking so as to build a framework for realizing different verification techniques, and making model checking as planning, problem-solving, scheduling/services.

Short Bio:

Dr Liu Yang graduated in 2005 with a Bachelor of Computing (Honours) in the National University of Singapore (NUS). In 2010, he obtained his PhD and started his post doctoral work in NUS, MIT and SUTD. In 2011, Dr Liu is awarded the Temasek Research Fellowship at NUS to be the Principal Investigator in the area of Cyber Security. In 2012 fall, he will serve as assistant professor in School of Computer Engineering, Nanyang Technological University.

Dr. Liu specializes in software verification using model checking techniques. His research has bridged the gap between the theory and practical usage of formal methods to evaluate the design and implementation of software for high assurance. His work led to the development of a state-of-the-art model checker, Process Analysis Toolkit (PAT). This tool is used by research institutions in over 50 countries for research and education.