Presenter: Xiaqing Zhou
Abstract: First, we introduce Unikernels, a lightweight operating system architecture that compiles application logic with minimal library dependencies into a single address space, contrasting it with traditional monolithic and modular OS designs. Additionally, we discuss DPDK (Data Plane Development Kit), a framework for high-performance packet processing in user space. The second focus is on the evolution of formal verification tools developed by Prof. Cao’s research group. We trace the progression from early verification frameworks to VST-A (Verified Software Toolchain-Advanced), a Coq-based system for proving functional correctness of C programs, as published in the landmark VST-A paper. Finally, we present the latest QCP tool, detailing its workflow for automating resource-aware verification through symbolic execution and constraint solving.