We are proud that our paper "BMCFuzz: Hybrid Verification of Processors by Synergistic Integration of Bound Model Checking and Fuzzing", has been accepted at International Conference on Computer-Aided Design(ICCAD) - 2025.
基础软件验证研究室是隶属于中国科学院软件研究所基础软件与系统重点实验室下的研究室，目前正在招收2025年推免生，欢迎大家报名！
我们诚挚欢迎具有强自我驱动力，具有较强计算机系统能力或数学基础，且对形式化方法和计算机软硬件系统形式化验证感兴趣的优秀学生加入我们的团队！
We joyfully celebrate the graduation of three outstanding master students: Yicheng Liu(刘易铖), Yifan Dong(董一凡) and Yiping Weng(翁一平). They have successfully completed their studies and are now ready to start new adventures in life and career.
We are proud that our paper "Training Verification-Friendly Neural Networks via Neuron Behavior Consistency", has been accepted at Thirty-Ninth AAAI Conference on Artificial Intelligence(AAAI25).
We are proud that our paper "Verification of Bit-Flip Attacks against Quantized Neural Networks", has been accepted at Object-Oriented Programming Systems, Languages and Applications (OOPSLA) - 2025.
We are proud that our paper "An efficient string solver for string constraints with regex-counting and string-length", has been accepted at Journal of Systems Architecture.
We are proud that our paper "LaserGuider: A Laser Based Physical Backdoor Attack against Deep Neural Networks", has been accepted at Network Security (ACNS).
We are proud that our paper "Formalization of Android Activity-Fragment Multitasking Mechanism and Static Analysis of Mobile Apps", has been accepted at Formal Aspects of Computing (FAC).
We are proud that our paper "SongBsAb: A Dual Prevention Approach against Singing Voice Conversion based Illegal Song Covers", has been accepted at Proceedings of the 32nd Annual Network and Distributed System Security Symposium (NDSS).
基础软件验证研究室为基础软件与系统重点实验室（中国科学院）2024年成立的核心研究单元，致力于用形式化验证技术来保障计算机软硬件基础设施的正确性与安全性。研究室成果发表在LICS、CAV、POPL、DAC、TACAS、CONCUR、IJCAR/CADE、Information and Computation等国际顶级会议与期刊上。研究室经费充足，研究室与国内外高校/研究所有着广泛的交流与合作。
由于研究室科研工作需要，现面向国内外诚聘高层次人才（副研究员/研究员），具体招聘研究方向如下：