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 recent research contributions in the system modeling, efficient model checking algorithms development and the application of formal verification in concurrent objects design, cyber physical systems, security, multi-agent systems and pervasive systems. 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. Since PAT is released 8 years ago, it has attracted 3500+ 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 joined School of Computer Engineering, Nanyang Technological University as a Nanyang Assistant professor.
Dr. Liu specializes in software verification, security and software engineering. 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 70 countries for research and education. He has more than 100 publications and leading a research group of 30 people.
