LoopInvGen: A Loop Invariant Generator based on Precondition Inference
We describe the LoopInvGen tool for generating loop invariants that can provably guarantee correctness of a program with respect to a given specification. LoopInvGen is an efficient implementation of the inference technique originally proposed in our earlier work on PIE (https://doi.org/10.1145/2908080.2908099). In contrast to existing techniques, LoopInvGen is not restricted to a fixed set of features -- atomic predicates that are composed together to build complex loop invariants. Instead, we start with no initial features, and use program synthesis techniques to grow the set on demand. This not only enables a less onerous and more expressive approach, but also appears to be significantly faster than the existing tools over the SyGuS-COMP 2018 benchmarks from the INV track.
Code (0)
등록된 구현이 없습니다.
Tasks
Program SynthesisSimilar Papers 제목 키워드 기반
InvWeaver: Deductive Feedback for Invariant Synthesis in Interacting-Loop Programs
Loop invariant inference is a fundamental yet challenging problem in program verification. Recent LLM-aided guess-and-check techniques have shown strong performance on single-loop programs, but they often struggle with p…
A Neurosymbolic Approach to Loop Invariant Generation via Weakest Precondition Reasoning
Loop invariant generation remains a critical bottleneck in automated program verification. Recent work has begun to explore the use of Large Language Models (LLMs) in this area, yet these approaches tend to lack a reliab…
Combining Mechanical and Agentic Specification Inference for Move
In this paper, we describe early work on a specification inference tool for the Move Prover that combines a weakest-precondition (WP) analysis over Move bytecode with an agentic coding CLI such as Claude Code. Specificat…
Loop Invariant Generation: A Hybrid Framework of Reasoning optimised LLMs and SMT Solvers
Loop invariants are essential for proving the correctness of programs with loops. Developing loop invariants is challenging, and fully automatic synthesis cannot be guaranteed for arbitrary programs. Some approaches have…
Logical ReasoningMeta-Learning with a Geometry-Adaptive Preconditioner
Model-agnostic meta-learning (MAML) is one of the most successful meta-learning algorithms. It has a bi-level optimization structure where the outer-loop process learns a shared initialization and the inner-loop process …
Few-Shot Image ClassificationFew-Shot LearningMeta-Learning