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.

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).

(2025年12月29日更新) 因工作需要，中国科学院软件研究所基础软件与系统重点实验室-基础软件验证研究室招聘硬件验证实习生若干名，详情如下：

岗位名称： 硬件验证科研实习生

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.

We are delighted to share that several members of the VerSys Group participated in the CCF ChinaSoft (中国软件大会) 2025 held in Wuhan, China.

We are proud that our paper "RunTyper: Enhancing Deep Type Inference Using Dynamic Analysis for Python", has been accepted at ACM Transactions on Software Engineering and Methodology (TOSEM) 2025.

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.