Research
Research Topics
Our group has been focusing on formal verification of both software and hardware. Currently, we are actively working on the following research topics:
-
Verification of RISC-V hardware designs: In order to improve the performance, more and more intelligent systems are using domain-specific CPUs. RISC-V is an open instruction set that supports rapid development of domain-specific CPUs and becoming increasingly popular. We focus on Chisel, a hardware construction language embedded in Scala for modular and parametric design of RISC-V CPUs. We investigate the techniques to achieve the automated verification of Chisel RISC-V CPU designs against the instruction-set compatibility and temporal properties. Moreover, we consider the formal verification of the compilation process of FIRRTL (an intermediate representation for Chisel) in proof assistants (e.g. Coq).
-
Operating system verification
-
Program verification: As the state-of-the-art safety-critical systems are usually developed with the C/C++ language and memory safety is a serious problem in these languages, we focus on the automated analysis and verification of memory safety in C/C++ languages, based on variants of separation logic. Moreover, we plan to investigate the memory safety issue of the Rust language, the increasingly popular language for developing system software. Moreover, the scripting languages (e.g. Javascript and Python) are also widely used in intelligent systems, we also investigate the verification of the programs in these languages, in particular, string constraint solving and symbolic execution of Javascript programs.
-
Verification of cryptographic systems
-
ReDoS defense
Publications and Tools
We have published a wide body of literature, see our publications page for details. Moreover, our group have developed multiple tools and applied them to several case studies. The main tools are: