Workshop on SAT/SMT and Model Checking

Time: 14:00-17:10, September 9th (Tuesday), 2025. 

Venue: Lecture room (334), the 3rd floor, Building 5, Software Park, Chinese Academy of Sciences. (Online Tencent Meeting No. 489-881-199)

Program: 

14:00-14:40, Philipp Rummer (University of Regensburg, Germany), What's Decidable About Arrays With Sums?

14:40-15:20, Shaowei Cai (ISCAS), Parallel Solving for SMT and MIP

15:20-15:50, Tea break

15:50-16:30, Qiusong Yang (ISCAS), The rIC3 Hardware Model Checker

16:30-17:10, Shaoke Cui (Beihang University), Z3-Noodler-Mocha: An Effective SMT Solver for Handling String Constraints

Information about the talks

What's Decidable About Arrays With Sums?

Abstract. The theory of arrays, supported by virtually all SMT solvers, is one of the most important theories in program verification. The standard theory of arrays, which provides read and write operations, has been extended in various different ways in past research, among others by adding extensionality, constant arrays, function mapping (resulting in combinatorial array logic), counting, and projections. In this talk, we will survey array theories extended with sum constraints, which capture properties of the sum of all elements of an integer array. Sum constraints are frequently used in program specifications, but are currently not supported by decision procedures or SMT solvers. As a main result, we show that the theory of extensional arrays extended with constant arrays and sum constraints can be decided in non-deterministic polynomial time. In contrast, adding sum constraints to combinatorial array logic gives rise to an undecidable theory.

The talk presents joint work with Roland Herrmann.

Speaker. Philipp Ruemmer (University of Regensburg)

Introduction of the speaker. 

Philipp Ruemmer is a professor of Theoretical Computer Science at the University of Regensburg. His research interests cover (but are not restricted to) the following areas: Theorem proving and decision procedures, SAT/SMT solving, Analysis of programs written in languages like Java, C#, C, C++, Simulink. He has built many well-known SMT solvers and model checkers, including the SMT solver Princess, the string solver OSTRICH, the Horn clause solver Eldarica, and the model checker JayHorn.  He will serve as the PC chair of CAV 2026. 

Parallel Solving for SMT and MIP

Abstract. Over the last years, we have witnessed tremendous advances in the effective and efficient parallelization of crucial constraint solving frameworks, such as propositional satisfiability (SAT), satisfiability modulo theories (SMT), and mixed integer programming (MIP). This talk provides an in-depth overview of parallelizations of SMT solving and MIP solving.

Speaker. Shaowei Cai (ISCAS)

Introduction of the speaker. 

Shaowei Cai is a professor of computer science, and he focuses on contraint solving and formal verification. He won more than 10 gold medals in SAT and SMT competitions, and won the Best/Distinguished Paper Award of CAV, SAT, CP. He serves as PC member in conferences including SAT, CP, FMCAD, ICAPS, and will serve as PC chair of SAT 2027. His solvers have been used in many EDA companies and software companies.

The rIC3 Hardware Model Checker

Abstract. In this presentation, we will  present rIC3, an efficient bit-level hardware model checker primarily based on the IC3 algorithm. It boasts a highly efficient implementation and integrates several recently proposed optimizations, such as the specifically optimized SAT solver, dynamically adjustment of generalization strategies, and the use of predicates with internal signals, among others. As a first-time participant in the Hardware Model Checking Competition, rIC3 was independently evaluated as the best-performing tool, not only in the bit-level track but also in the word-level bit-vector track through bit-blasting. Our experiments further demonstrate significant advancements in both efficiency and scalability. rIC3 can also serve as a backend for verifying industrial RTL designs using SymbiYosys. Additionally, the source code of rIC3 is highly modular, with the IC3 algorithm module being particularly concise, making it an academic platform that is easy to modify and extend.

Speaker. Qiusong Yang (ISCAS)

Introduction of the speaker. Qiusong Yang is currently a Research Professor and Ph.D. Supervisor at the Institute of Software, Chinese Academy of Sciences. His main research interests include software engineering, model checking, software/hardware co-design. He has led several national and academy-level projects, including the National Science and Technology Major Projects, the Chinese Academy of Sciences Strategic Priority Research Program, the National Natural Science Foundation of China, etc.. He has published papers in conferences such as ICSE, AAAI, MICRO, DAC, and CAV, and has received the ACM SIGSOFT Distinguished Paper Award and the CAV Distinguished Paper Award.

Z3-Noodler-Mocha: An Effective SMT Solver for Handling String Constraints

Abstract. This talk introduces Z3-Noodler-Mocha, an effective SMT solver designed to deal with string constraints. By applying multiple optimization techniques, such as constraint extraction and automata optimization, Z3-Noodler-Mocha significantly reduces the search space of Nielsen transformation and stabilization-based procedures. Demonstrating its effectiveness, Z3-Noodler-Mocha won the QF_Strings Division at the International SMT Competition 2025, achieving substantial performance improvements over state-of-the-art string solvers.

Speaker. Shaoke Cui (Beihang University)

Introduction of the speaker. Shaoke Cui is a PhD student at the School of Software, Beihang University, where he focuses on constraint solving under the supervision of Prof. Chunming Hu and Dr. Chuan Luo. He has published 2 papers in top-tier computer science conferences, including ICSE 2026 and ASE 2025. His developed SMT solver, Z3-Noodler-Mocha, was the winner of the QF_Strings Division at the International SMT Competition 2025. In addition, he has awarded multiple gold medals in the Asia Regional Contests of the International Collegiate Programming Contest (ICPC).