CCF-Huawei Project Proposal Granted

Our project proposal has been granted for funding by the CCF-Huawei Populus Grove Fund.

Our project proposal titled “Modular Verification by Integrating Large Language Models with Symbolic Reasoning” has been granted for funding by the joint Populus Grove Fund of the China Computer Federation (CCF) and Huawei. This project aims to develop a lightweight verification (and testing) framework for operating system kernels by leveraging the integrated power of large language models (mainly for specification synthesis) and symbolic reasoning techniques (e.g., static analysis, symbolic execution, and automated theorem proving). The key to this framework is a fine-grained, compositional procedure of refining verification specifications and obligations.