基础软件验证研究室
Research Group on Verification of System Software (VerSys)
中国科学院软件研究所
基础软件与系统重点实验室（计算机科学国家重点实验室）
Institute of Software, Chinese Academy of Sciences
欢迎来到基础软件验证研究室的主页！研究室专注于形式化验证技术在计算机软硬件上的应用，尤其是保障基础软件（如操作系统、编译器）的正确性及安全性。
Welcome to the VerSys group website! Our research group focuses on applying formal verification techniques to both software and hardware, with an emphasis on ensuring the correctness and security of foundational system software, such as operating systems and compilers.
We welcome like-minded researchers and students to join us! Currently multiple positions are open in our group, including full/associate research professors, postdocs, engineers and interns (processor verification/OS verification). Feel free to apply!
Group members
The VerSys group is led by Zhilin Wu, assisted by a few faculty members and several master and Ph.D students in its research and teaching activities. More information about the members of our group can be found in the group members page.
Research
The VerSys group is very active in applying formal methods to several practical problems, such as the verification of RISC-V hardware designs, OS verification, program verification, and the security of network systems. Our research results in a number of publications, providing new theoretical results that are supported and confirmed by tools developed by the group members. Please check the research page for more details.
Teaching
Besides their research duties, the VerSys group members are also in charge of giving courses on different topics.
Other activities
The VerSys group members enjoy taking part in several other activities, such as seminars and badminton games together with our visitors.