Research Projects
Current Projects
We develop systematic tools, theories, and methodologies for ensuring the correctness, reliability, and efficiency of software and systems, focusing on automated techniques such as model checking, machine learning, and program analysis. Our work targets several different kinds of advanced software/systems, including critical infrastructure, autonomous vehicles, and smart contracts.
Concurrency
Concurrency bugs are the result of unexpected unwanted thread/process coordination. They are extremely hard to identify and eliminate. In this line of work, we aim to tackle the problem from different aspects.
Neural Network Testing, Verification & Repair
Neural networks can be (arguably) viewed a different paradigm of programming, where logical reasoning is replaced with big data and optimization. Unlike traditional programs, however, neural networks are subject to bugs, e.g., adversarial samples and discriminatory instances. In this line of work, we aim to develop systematic theories, methods and tools to improve the quality of AI-systems.
Smart Contracts Analysis
Smart contracts are blockchain based contracts which bind multiple parties through executable programs. “Code is Law”! They are believed to revolutionize many industries. Like traditional programs, smart contracts may suffer from bugs and vulnerabilities. Unlike traditional programs, due to the nature of blockchain, smart contracts cannot be easily patched. It is thus important that smart contracts are thoroughly tested or, even better, verified.
Testing/Defending CPSs
Cyber-physical systems are often safety-critical, e.g., those which control important infrastructure such as water and electricity. They thus must be systematically analyzed.
Past Projects
The following are some past research projects that we have completed.