PAT project is initialized in School of Computing, National Univeristy of Singapore in July 2007. Our group is listed below.

The key members of PAT:

• Dr. SUN, Jun, Assistant Professor, Singapore University of Technology and Design.
• Dr. LIU, Yang, Assistant Professor, School of Computer Engineering, Nanyang Technological University.
• Dr. DONG, JinSong, Associate Professor, School of Computing, National University of Singapore.

Current Postdoc

• Dr. LIN Shang-Wei, Compositional verification and synthesis with assume-guarantee reasoning.
• ZHANG Xian, Modeling and verifying timed systems and pervasive computing systems.

Current Ph.D Students

• ZHU, Huiquan, Model checking C# program.
• ZHANG Shaojie, Formal verification of UML and distributed systems, event-based model checking and symmetry reduction.
• ZHENG Manchun, Automatic verification of WSN software, developing NesC@PAT.
• SONG Songzheng, Probabilistic model checking.
• TAN Tian Huat, Verification of Web Service Composition, working on Orc Module for PAT.
• LIU Yan, Model checking in smart space; Reasoning and verification of context-aware applications.
• SHI Ling, UTP Semantics of PAT modeling languages.
• GUI Lin, Software Reliability Analsysis, statistical model checking.
• Truong Khanh Nguyen, Symbolic model checking.
• BAI Guangdong
• JI Kun
• CHEN Manman

Research Assistants

• XIAO Hao, Assembly code model checking.
• MA Junwei

Undergraduate Students

• Nguyen Chi Dat, Multi-core model checking.

Visiting Students and researchers

• SI Yuanjie, from Zhejiang University, China.
• HAO Jianye, from the Chinese University of Hong Kong.
• Pakorn Waewsawangwong, April 2011, from University of York, UK.
• Prof WANG Xinyu, July – Sep 2011, from ZJU, China. VLS information system, software re-engineering, trustworthy software and financial information system.

Previous PAT members:

• Dr. David Sanan, Formal verification of software at source code level.
• Dr. CHEN Chunqing
• Dr. Étienne André, Model checking Timed systems and Parametric Timed Automata, and techniques in parameter synthesis.
• ZHANG Jiexin, Modeling and verification of Event-Grammar.
• Dr. Henri Hansen, partial order reduction

Should you meet any difficulty using PAT or find bugs of PAT or have some suggestion on improving PAT, please do not hesitate to contact any one of us. Alternatively, you can send an email to “pat at comp dot nus dot edu dot sg” (replace dot with ‘.’).