I am interested in developing systematic tools/theories/methodologies for software/system correctness, reliability and efficiency. My current focus is on automated system verification techniques, in particular, model checking. I am interested in publishing at the following top-tier conferences and journals: CAV, ICSE, FSE, FM, TACAS, IEEE Transactions on Software Engineering, ACM Transactions on Software Engineering and Methodology, etc. A big part of my recent research is on a model checking framework called PAT. To this date (3.5.14), PAT has attracted more than 3000 registered users from more than 300 organizations. It has been used to teach formal methods and model checking in multiple universities and companies.
Education and Working Experience
- 2010 – Present, Assistant Professor, SUTD
- 2011 – 2012, Visiting Scholar, MIT
- 2007 – 2010, LKY Postdoctoral Fellow, School of Computing, NUS
- 2006 – 2007, Postdoctoral Fellow, School of Computing, NUS
- 2002 – 2006, Research Assistant and Part-Time PhD, School of Computing, NUS
- 1998 – 2002, Bachelor of Computer Science, School of Computing, NUS
- Program co-Chair of 20th International Symposium on Formal Methods (FM 2014)
- General co-Chair of 18th IEEE International Conference on the Engineering of Complex Computer Systems (ICECCS 2013)
- Program co-Chair of 4th IEEE International Conference on Secure Software Integration and Reliability Improvement (SSIRI 2010)
- Program Committee of ICSE-NIER 2015, AVOCS 2014, ICECCS 2014, ICFEM 2014, UTP 2014, TIME 2014, SEFM 2014, SSV 2014, TIME 2013, ICFEM 2013, FORMATS 2013, FSE 2013 (tool demo track), SSV 2012, TASE 2012, UTP 2012, APSEC 2012, ICFEM 2012, ICFEM 2011, MODELS 2011, SSIRI 2011, IJCAI 2011, MODELS 2010, ICFEM 2010, ATVA 2010, UTP 2010, TASE 2009, ICIS 2009
- Yun Lin, Zhenchang Xing, Yinxing Xue, Yang Liu, Xin Peng, Jun Sun, and Wenyun Zhao. Detecting and Summarizing Differences across Multiple Instances of Code Clones. 36th International Conference on Software Engineering (ICSE 2014).
- Tian Huat Tan, Manman Chen, Étienne André, Jun Sun, Yang Liu and Jin Song Dong. Automated Runtime Recovery for QoS-based Service Composition.International World Wide Web Conference (WWW), 2014.
- Ting Wang, Jun Sun, Yang Liu, Xinyu Wang and Shanping Li. Language Inclusion Checking for Timed Automata. 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2014.
- Shang-Wei Lin, Etienne Andre, Yang Liu, Jun Sun, and Jin Song Dong. Learning Assumptions for Compositional Verification of Timed Systems. IEEE Transactions on Software Engineering, 2014.
- Jun Sun, Yang Liu, Jin Song Dong, Yang Liu, Jin Song Dong, Yan Liu, Ling Shi and Etienne Andrew. Modeling and Verifying Hierarchical Real-time Systems using Stateful Timed CSP. ACM Transactions on Software Engineering and Methodology, 2013.
Program Analysis through Testing, Learning and Verification (TLA)Securify: A Compositional Approach of Building Security Verified System, SUTD-ASPIRE: Design of Secure Cyber Physical Systems, Cyber-Physical System Protection, Advancing Security of Public Infrastructure with Resilience and Economics