About Me

A chinese lion statue

I am a Nanyang assistant professor in Division of Software and Information Systems (SIS), School of Computer Science and Engineering, Nanyang Technological University. My current research interests are related to Formal Methods, Security, Software Engineering and Multi-Agent systems.

For model checking algorithms and tools, we are developing a model checker development framework Process Analysis Toolkit (PAT) development, which is a self-contained framework to support composing, simulating and reasoning of various systems (e.g., concurrent and real-time systems, probabilistic systems, web-service, security protocols, sensor networks, software architecture description language and so on).

For cybersecurity, we are working at malware modeling, detection, classification and generation with the focus on Javascript malware (refer to AsiaCCS 2015 and ISSTA 2015 papers), desktop malware and Android malware (AsiaCCS 2016, IJCNN 2016, ISSTA 2016, TSE 2017). We are developing tools for vulnerability modeling and detection using machine learning and (both static and dynamic) program analysis on binary code (FSE 2016, ICSE 2017, S&P 2017, FSE 2017). In our Securify research project (2015- 2020), we are performing formal verification on security system from hardware (FM 2016 paper), hypervisor (ISSRE 2015, TACAS 2016, TACAS 2017, TDSC 2017), programs to security protocol (TSE 2017) using different verification approaches. Recently, we embark on the research on Automotive Security and autonomous vehicle Security in their security design, runtime security monitoring and response, and also the security testing and certification.

For software engineering, we are working on the topics related to program specification learning and model learning (ASE 2013 and FSE 2015 papers), performance analysis (ICSE 2016 paper), energy analysis (TMC 2016 paper), reliability analysis (ISSTA 2014 paper), code clone analysis (ICSE 2014 FSE 2016 and ASE 2017 papers), program debugging (ICSE 2017 paper), program testing (FSE 2017 paper), automatic loop analysis (ISSTA 2015, FSE 2016, FSE 2017 and ASE 2017 papers) using techniques like model checking, symbolic execution and machine learning. We are building tools related to these aspects.

For multi-agent systems, we are working on the topics related to formal modeling of various multi-agent systems, particularly trust management systems and their analysis in correctness, security and robustness (AAAI, IJCAI, AAMAS amd JAIR papers).

For big data, we are promoting the concept called event analytic based on behavior learning and analysis, and their applications in sports and finance systems (refer to our ICTAC 2014 and TASE 2015 invited papers).


Room No: 02C-82, Block N4
School of Computer Science and Engineering, Nanyang Technological University
50 Nanyang Avenue, Singapore 639798

Direction to get to my office

E-mail: yangliu AT ntu.edu.sg
Office Tel: +65-67906706
Fax: +65-67926559


  • 18 July 2017: Two full paper accepted by ASE 2017: "Mining Implicit Design Templates for Actionable Code Reuse" and "FiB: Squeezing Loop Invariants by Interpolation between Forward/Backward Predicate Transformers" (Acceptance rate: 20.7% = 65/314)
  • 2 June 2017: Three full paper accepted by ESEC-FSE 2017: "Guided, Stochastic Model-Based GUI Testing of Android Apps", "Steelix: Program-State Based Binary Fuzzing", and "Loopster: Static Loop Termination Analysis" (Acceptance rate: 24%=72/295)
  • 29 May 2017: Journal paper accepted by IEEE Transactions on Software Engineering (TSE): "A Formal Specification and Verification Framework for Timed Security Protocols"
  • 11 May 2017: Joined PC member of ISSTA 2018, submit your paper.
  • 19 March 2017: Full paper accepted by IEEE Transactions on Software Engineering (TSE): "Towards Model Checking Android Applications"
  • 26 Feb 2017: Full paper accepted by DAC 2017: "No-Jump-into-Basic-Block: Enforce Basic Block CFI on the Fly for Real-world Binaries"
  • 25 Feb 2017: Journal paper accepted by IEEE Transactions On Systems, Man, And Cybernetics: Systems (TSMC): "Collision and Deadlock Avoidance in Multirobot Systems: A Distributed Approach"
  • 16 Feb 2017: Journal paper accepted by Transactions on Dependable and Secure Computing (TDSC): "Refinement-based Specification and Security Analysis of Separation Kernels"
  • 10 Feb 2017: Full paper accepted by Security and Privacy (Oakland 2017): "Skyfire: Data-Driven Seed Generation for Fuzzing"
  • 16 Jan 2017: Journal paper accepted by IEEE Transactions on Information Forensics & Security (TIFS): "Auditing Anti-Malware Tools by Evolving Android Malware and Dynamic Loading Technique."
  • 23 Dec 2016: Full paper accepted by TACAS 2017: "CSimpl: a Framework for the Verification of Concurrent Programs using Rely-Guarantee."
  • 13 Dec 2016: Two full papers accepted by ICSE 2017: "Feedback-Based Debugging" and "SPAIN: Security Patch Analysis for Binaries - Towards Understanding the Pain and Pills."
  • 03 Dec 2016: Joined PC member of TACAS 2018, submit your paper.
  • 21 Oct 2016: FSE 2016 SIGSOFT Distinguished Paper Award: "Proteus: Computing Disjunctive Loop Summary via Path Dependency Analysis"
  • 3 Oct 2016: Journal paper accepted by Journal of Artificial Intelligence Research (JAIR): "MOCA: Modeling and Analysis of Agent Behaviors in Commitment Protocols"
  • 8 Aug 2016: Full paper accepted by FM 2016: "An Executable Formalisation of the SPARCv8 Instruction Set Architecture: A Case Study for The LEON3 Processor"
  • 1 Aug 2016: Best Paper Award at 10th IFIP WG 11.11 International Conference on Trust Management (IFIPTM) 2016: "How to Use Information Theory to Mitigate Unfair Rating Attacks"
  • 1 Aug 2016: Tim Muller joins University of Oxford as a Lecturer. Congratulations!
  • 25 July 2016: Full paper accepted by IEEE Transactions on Mobile Computing: "Battery-Aware Mobile Data Service"
  • 13 July 2016: Full paper accepted by IEEE Transactions on Services Computing: "Architecture-Based Behavioral Adaptation with Generated Alternatives and Relaxed Constraints"
  • 28 May 2016: Two full papers accepted by FSE 2016: "Proteus: Computing Disjunctive Loop Summary via Path Dependency Analysis" and "BinGo: Cross-Architecture Cross-OS Binary Search"
  • 19 April 2016: Full paper accepted by ISSTA 2016: "Semantic Modelling of Android Malware for Effective Malware Comprehension, Detection and Classification".
  • 15 March 2016: Journal paper accepted by IEEE Transactions on Very Large Scale Integration Systems: "A Fine-Grained Control Flow Integrity Approach Against Runtime Memory Attacks Using Hardware-Enhanced Architecture for Embedded Systems".
  • 5 Feb 2016: Full paper accepted by AsiaCCS 2016: "Mystique: Evolving Android Malware for Auditing Anti-Malware Tools". (Acceptance rate: 73/350=20.9)
  • 18 Dec 2015: Full paper accepted by TACAS 2016: "Reasoning About Information Flow Security of Separation Kernels with Channel-based Communication"
  • 16 Dec 2015: Two full papers accepted by ICSE 2016: "Generating Performance Distributions via Probabilistic Symbolic Execution" and "Optimizing Selection of Competing Services with Probabilistic Hierarchical Refinement."
  • 13 Nov 2015: Full paper accepted by AAAI 2015: "Is it Harmful when Advisors only Pretend to be Honest? "
  • 3 Oct 2015: 2015 Best Paper Award for Journal of Software and Systems Modeling: "Formalizing and Verifying Stochastic System Architectures Using Monterey Phoenix", award letter
  • 5 Aug 2015: Journal paper accepted by IEEE Transactions on Information Forensics & Security (TIFS): "Semantics-based Online Malware Detection: Towards Efficient Real-time Protection Against Malware"
  • 25 July 2015: Joined PC member of ASE 2016, submit your paper and visit Singapore in September 3-7, 2016.
  • 18 July 2015: Full paper accepted by ASE 2015: "Interpolation Guided Compositional Verification"
  • 27 May 2015: Full paper accepted by FSE 2015: "TLV: Abstraction through Testing, Learning and Validation"
  • 1 May 2015: Journal paper accepted by ACM Computing Surveys: "Collaborative Security: A Survey and Taxonomy" PDF Download
  • 29 April 2015: Full paper accepted by IJCAI 2015: "Quantifying Robustness of Trust Systems Against Collusive Unfair Rating Attacks Using Information Theory"
  • 1 April 2015: Four full papers accepted by ISSTA 2015
  • 24 March 2015: Two full papers accepted by FM 2015
  • 28 Jan 2015: Two full Papers accepted by AAMAS 2015
  • 22 Dec 2014: Full Paper accepted by AsiaCCS 2015 "JSDC: A Hybrid Approach for JavaScript Malware Detection and Classification" (?/269 submission)
  • 9 Nov 2014: Full Paper accepted by AAAI 2015 "Automated Analysis of Commitment Protocols using Probabilistic Model Checking"
  • 18 Sep 2014: Paper accepted by TSE "A Systematic Study on Explicit-state Non-Zenoness Checking for Timed Automata"
  • 23 June 2014: Full paper accepted by ICSME 2014 "Clonepedia: Summarizing Code Clones by Common Syntactic Context for Software Maintenance" (40/210=19% acceptance rate)
  • 20 June 2014: Four papers accepted by ICFEM 2014 (30% acceptance rate)
  • 19 April 2014: Full paper accepted by CAV 2014 "Diamonds are a Girl's Best Friend: Partial Order Reduction for Timed Automata With Abstractions"
  • 17 Feb 2014: Full paper accepted by FM 2014 Industry Track "MDP-based Reliability Analysis of an Ambient Assisted Living System"
  • 17 Feb 2014: Demo paper accepted by ICSE 2014 "VeriWS: A Tool for Verification of Combined Functional and Non-functional Requirements of Web Service Composition" (15/41=36.5% acceptance rate)
  • 14 Feb 2014: Demo paper accepted by AAMAS 2014 "An Extensive Model Checking Framework for Multi-agent Systems"
  • 1 Feb 2014: Two papers accepted by FM 2014 "Formal Verification of Operational Transformation" and "TrustFound: Towards a Formal Foundation for Model Checking Trusted Computing Platforms" (38/135=28% acceptance rate)
  • 16 Jan 2014: Paper accepted by ICSE 2014 "Detecting and Summarizing Differences across Multiple Instances of Code Clones" (99/495=20% acceptance rate)
  • 28 Dec 2013: Paper accepted by WWW 2014 "Automated Runtime Recovery for QoS-based Service Composition" (84/650=12.9% acceptance rate)
  • 21 Dec 2013: Paper accepted by TACAS 2014 "Language Inclusion Checking for Timed Automata" (26 out of 117 research papers: 22.2%)
  • 29 Nov 2013: Paper accepted by TSE "Learning Assumptions for Compositional Verification of Timed Systems"
  • 28 Nov 2013: tier 1 grant received "Bring the Advanced Model Checking Techniques to Real-world Problems"
  • 4 Sep 2013: Paper accepted by APSEC 2013 "Multi-core Algorithms for LTL Verification"
  • 19 Aug 2013: I am looking for both master and ph.d. students. Scholarship will be provided for ph.d. candidates only.
  • 18 Aug 2013: we are orgnizing FM 2014 in Singapore. The CFP is ready now.
  • 25 July 2013: three papers accepted by ASE 2013 (accept rate 43/317=13.6%)
  • 21 June 2013: Tool paper accepted by FSE 2013 "USMMC: A Self-Contained Model Checker for UML State Machines"
  • 19 June 2013: Four papers accepted by ICFEM 2013
  • 5 June 2013: Tool Paper accepted by ATVA 2013 "CELL: A Compositional Verification Framework"
  • 1 May 2013: Paper accepted by ISSTA 2013 "Combining Model Checking and Testing with an Application to Reliability Prediction and Distribution"
  • 19 April 2013: Paper accepted by SPIN 2013 "Verifying a Quantitative Relaxation of Linearizability via Refinement"
  • 4 April 2013: two paper accepted by iFM 2013 "Speed Up Verification in DTMC via Divide and Conquer" and "A Formal Semantics for the Complete Syntax of UML State Machines with Communications"
  • 7 March 2013: Paper accepted by CAV 2013 "PSyHCoS: Parameter Synthesis for Hierarchical Concurrent Real-Time Systems"
  • 26 Feb 2013: Awarded Nanyang Assistant Professor.
  • 22 Jan 2013: PAT Tutorial "Build Your Own Model Checker in One Month" is accepted by ICSE 2013.
  • 20 Nov 2012: I am looking for self-motivated Ph.D. students and research assistants on the area of formal methods, security, program analysis and software engineering.
    Please email me with your CV if interested.
  • 20 Nov 2012: Postdoc Research Fellow Positions on Model Checking and/or Security are Available!
    I am currently looking for postdoc research fellow on model checking on security verification. All interested candidates are welcomed to apply. Kindly send your CV to me via email. The compensation package is highly competitive internationally. Details about the positions can be found HERE.


  • July 2005 - May 2010, National University of Singapore, Singapore
    Ph.D. (CAP 4.56/5)
    Thesis: Model Checking Concurrent and Real-time Systems: the PAT Approach
    Supervisors: Dr. Dong JinSong and Dr. Rudy Setiono.
    Nominated for best thesis.
  • July 2001 - Jun 2005, National University of Singapore, Singapore
    Bachelor of Computing Science with Honour First Class. (CAP 4.83/5)
    Mathematics Minor
  • Dec 2000 - Jun 2001, National Institute of Education, Singapore
    Intensive English training course.
  • Sep 2000 - Nov 2000, Zhe Jiang University, China
    Electrical Engineering in an accelerated class. Received scholarship from Ministry of Education, Singapore after two months.

Awards and Scholarship

  • Nanyang Assistant Professor 2013
  • Best Paper Award: Yan Liu, Xian Zhang, Yang Liu, Jun Sun, Jin Song Dong, Jit Biswas and Mounir Mokhtari. Formal Analysis of Pervasive Computing Systems. The 17th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2012), Paris, France, July 18 - 20, 2012
  • Best Paper Award: The 4th IEEE International Conference on Secure Software Integration and Reliability Improvement (SSIRI 2010), 2010.
  • Nominated for President's Science Award 2010 together with Dr JinSong Dong and Dr Jun Sun.
  • Nominated for Best Ph.D. Thesis, NUS 2010.
  • Dean's Graduate Research Excellence Award 2009/2010
  • Research Achievement Award 2008/2009
  • Microsoft Asia Research Fellowship 2007
    The annual Microsoft Fellowship Program is designed to support talented PhD students who have the potential to become future research leaders. Over the past seven years, 159 recipients have participated in the program. Fellowships have been awarded to outstanding students from more than 30 universities and research institutes throughout the Asia-pacific Region since 1999.
  • Graduate Scholarship in National University of Singapore, 2005 - 2009.
  • Tata Consultancy Services Asia Pacific Medal and Prize
    The second best graduate throughout the course of study for the Bachelor of Computing (Honours) in the School of Computing, NUS. (2nd of 800+ students with CAP 4.83/5).
  • No. 4 in Microsoft Imagine Cup Competition, Singapore, 2005 May
    We are a gang of four: Guo Liang, Huang Wenfan, Liu Yang (team leader) and Ng Junping. We developed the eWorld System, which is a sign language capturing and interpretation system, supervised by Dr Huang Zhiyong.
  • Place on Dean's List in academic season 2004/2005
  • Place on Dean's List in academic season 2003/2004
  • Place on Dean's List in academic season 2002/2003
  • Place on Dean's List in academic season 2001/2002.
  • Undergraduate Scholarship for PRC Students from MOE, 2000 - 2005.