ISSTA 2025
Wed 25 - Sat 28 June 2025 Trondheim, Norway
co-located with FSE 2025
Fri 27 Jun 2025 11:25 - 11:50 at Cosmos 3B - Program Analysis 2 Chair(s): Alexi Turcotte

Loop invariant inference is a fundamental, yet challenging, problem in program verification. Recent work adopts the guess-and-check framework, where candidate loop invariants are iteratively generated in the guess step and verified in the check step. A major challenge of this general framework is to produce high-quality candidate invariants in each iteration so that the inference procedure can converge quickly. Empirically, we observe that existing approaches may struggle with guessing the complete invariant due to the complexity of logical connectives, but usually, all the clauses of the correct loop invariant have already appeared in the previous guesses. This motivates us to refine the guess-and-check framework, resulting in a generate-combine-check framework, where the loop invariant inference task is divided into clause generation and clause combination. Specifically, we propose a novel loop invariant inference approach Clause2Inv under the new framework, which consists of an LLM-based clause generator and a counterexample-driven clause combinator. As the clause generator, Clause2Inv leverages LLMs to generate a multitude of clauses; as the clause combinator, Clause2Inv leverages counterexamples from the previous rounds to convert generated clauses into invariants. Our experiments show that Clause2Inv significantly outperforms existing loop invariant inference approaches. For example, Clause2Inv solved 312 (out of 316) linear invariant generation tasks and 44 (out of 50) nonlinear invariant generation tasks, which is at least 93 and 16 more than the existing baselines, respectively. By design, the generate-combine-check framework is flexible to accommodate various existing approaches which are currently under the guess-and-check framework by splitting the guessed candidate invariants into clauses. The evaluation shows that our approach can, with minor adaptation, improve existing loop invariant inference approaches in both effectiveness and efficiency. For example, Code2Inv which solved 210 problems with an average solving time of 137.6 seconds can be improved to solve 252 problems with an average solving time of 17.8 seconds.

Fri 27 Jun

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

11:00 - 12:15
Program Analysis 2Research Papers at Cosmos 3B
Chair(s): Alexi Turcotte CISPA
11:00
25m
Talk
Bridging the Gaps Between Graph Neural Networks and Data-Flow Analysis: The Closer, the Better
Research Papers
Qingchen Yu Zhejiang University, Xin Liu Lanzhou University, Qingguo Zhou Lanzhou University, Chunming Wu Zhejiang University
DOI
11:25
25m
Talk
Clause2Inv: A Generate-Combine-Check Framework for Loop Invariant Inference
Research Papers
Weining Cao Nanjing University, China, Guangyuan Wu Nanjing University, China, Tangzhi Xu Nanjing University, China, Yuan Yao Nanjing University, Hengfeng Wei State Key Laboratory for Novel Software Technology, Nanjing University, Taolue Chen Birkbeck, University of London, Xiaoxing Ma Nanjing University
DOI
11:50
25m
Talk
Incremental Verification of Concurrent Programs through Refinement Constraint Adaptation
Research Papers
Liangze Yin National University of Defense Technology, Yiwei Li , Kun Chen National University of Defense Technology, Wei Dong National University of Defense Technology, Ji Wang National University of Defense Technology
DOI

Information for Participants
Fri 27 Jun 2025 11:00 - 12:15 at Cosmos 3B - Program Analysis 2 Chair(s): Alexi Turcotte
Info for room Cosmos 3B:

Cosmos 3B is the second room in the Cosmos 3 wing.

When facing the main Cosmos Hall, access to the Cosmos 3 wing is on the left, close to the stairs. The area is accessed through a large door with the number “3”, which will stay open during the event.

:
:
:
: