Skip to main content

中国科学院软件研究所基础软件验证研究室2026年推免生招收启事

· 3 min read

基础软件验证研究室是隶属于中国科学院软件研究所基础软件与系统重点实验室下的研究室，目前正在招收2026年推免生，欢迎大家报名！

我们诚挚欢迎具有强自我驱动力，具有较强计算机系统能力或数学基础，且对形式化方法理论和工具、计算机基础软硬件系统的形式化验证感兴趣的优秀学生加入我们的团队！

Congratulations to Three Graduates

· One min read

We warmly congratulate Weizhi Feng (冯维直) and Denghang Hu (胡登杭) on receiving their Ph.D. degrees, and Shidong Shen (申世东) on receiving his master's degree. Their hard work, persistence, and dedication throughout their studies are sincerely celebrated by the group.

Paper accepted at ISSTA'26

· One min read

We are proud that our paper "Augmenting Multi-Technique Static Analysis with Large Language Models: A Neuro-Symbolic Approach to Smart Contract Vulnerability Detection" has been accepted at The ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA).

Paper on RISC-V ISA Conformance Model Checking Accepted at JSA'26

· One min read

We are proud that our paper "χRVFormal: Formal Verification of RISC-V Processor Chisel Designs", has been accepted at Journal of Systems Architecture (JSA) 2026.

χRVFormal presents the first end-to-end approach for formally verifying RISC-V processor designs entirely at the Chisel high-level. By constructing a modular, parameterized reference model in Chisel and devising a novel synchronization mechanism, it reduces verification to a model-checking problem applicable to both in-order and out-of-order processors. Evaluated on riscv-mini, NutShell, and BOOM, our tool significantly outperforms state-of-the-art methods, discovering 7 real-world unknown bugs and achieving three orders of magnitude higher efficiency.

Paper accepted at FM'26

· One min read

We are proud that our paper "Can LLM Aid in Solving Constraints with Inductive Definitions?", has been accepted at 27th Symposium on Formal Methods (FM) 2026.

Paper accepted at TDSC'26

· One min read

We are proud that our paper "AudioJailbreak: Jailbreak Attacks against End-to-End Large Audio-Language Models", has been accepted at IEEE Transactions on Dependable and Secure Computing (TDSC).

Paper accepted at FSE'26

· One min read

We are proud that our paper "SmartIFSyn: Automated Information Flow Security Policy Synthesis for Smart Contracts", has been accepted at ACM International Conference on the Foundations of Software Engineering (FSE) 2026.