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等国际顶级会议与期刊上。研究室经费充足，研究室与国内外高校/研究所有着广泛的交流与合作。

由于研究室科研工作需要，现面向国内外诚聘高层次人才（副研究员/研究员），具体招聘研究方向如下：

• 交互式定理证明
• 操作系统验证
• 硬件设计验证
• 程序分析与验证
• SAT/SMT求解
• 模型检测
• 抽象解释

因工作需要，中国科学院软件研究所基础软件与系统重点实验室（计算机科学国家重点实验室）基础软件验证研究室招聘硬件验证实习生若干名，详情如下：

岗位名称： RISC-V处理器设计测试、仿真、验证实习生

因工作需要，中国科学院软件研究所基础软件与系统重点实验室（计算机科学国家重点实验室）基础软件验证研究室招聘操作系统验证实习生若干名，详情如下：

岗位名称： 操作系统验证实习生

Mini-course on Automata and Transducers (8 hours)

授课老师：Professor Mikolaj Bojanczyk (Warsaw University)

课程摘要：In my mini-course, I will show how the humble finite automaton is, in fact, an extraordinarily flexible machine, which can be adapted to objects such as infinite words or trees, and enjoys an interesting and mathematically non-trivial theory. Also, there is a deep connection between automata and other fields, such as logic and semigroup theory. The mini-course will consist of four parts, each one with two hours.