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.
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.
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.
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.
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.
The following are some past research projects that we have completed.