We are proud that our paper "Decision Procedures for A Theory of String Sequences", has been accepted at 23rd Asian Symposium on Programming Languages and Systems (APLAS).

We are proud that our paper "A Formally Verified Procedure for Width Inference in FIRRTL", has been accepted at 35th European Symposium on Programming.

ESOP is an annual conference devoted to fundamental issues in the specification, design, analysis, and implementation of programming languages and systems, and is one of the conferences of ETAPS (European Joint Conferences on Theory and Practice of Software).

We are proud that our paper "OSTRICH: Solver for Complex String Constraints", has been accepted at Formal Methods in Computer-Aided Design 2025(FMCAD 2025).

We are proud that our paper "Separation Logic with Heap Variables: A Decision Procedure and Its Application", has been accepted at The Symposium on Dependable Software Engineering Theories, Tools and Applications (SETTA) - 2025.

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.