一句话：系统实验揭示位向量程序中模板不变式生成的模板与求解器影响，并证明其可处理现有方法难处理的基准。
基于模板的不变式生成是一种参数化且相对完备的循环不变式推断方法，但其在位精确推理（以位向量算术建模整数）上的进展有限，而这对忠实刻画机器整数语义并保证程序验证的可靠与精确至关重要。本文作为经验论文，从三方面系统实验研究位精确、基于模板的不变式生成：不同不变式模板的精度、不同约束求解器求解约束的性能，以及该方法与现有位精确验证技术相比的有效性。作者在广泛基准上开展大规模评估，发现模板与约束求解器的选择会不同程度地影响不变式生成的精度和效率；同时，基于模板的方法能够处理其他位向量方法无法处理的基准。结果还为未来研究提供了若干指导。
The template-based approach to invariant generation is a parametric and relatively complete methodology for inferring loop invariants. The relative completeness ensures the generated invariants' accuracy up to the template's form and the inductive condition. However, there has been limited in advancing the approach to bit-precise reasoning, which involves modeling integers using bit-vector arithmetic. This is unfortunate because bit-precise reasoning is crucial for faithfully and accurately modeling machine integer semantics and, thus, for ensuring sound and precise program verification. In this experience paper, we present an experimental study of bit-precise, template-based invariant generation on three fronts: the precision of different invariant templates, the performance of different constraint solvers for solving the constraints, and the effectiveness of the template-based approach compared to existing bit-precise verification techniques. Through an extensive experimental evaluation over a wide range of benchmarks, we find that (1) the choices of invariant templates and constraint solvers have varying degrees of impact on the precision and efficiency of invariant generation; (2) the template-based approach can handle benchmarks that other approaches for bit-vectors cannot handle. The results also reveal several guidelines for advancing future research on template-based invariant generation.
@inproceedings{YaoKSFWR23,
title = {Demystifying Template-Based Invariant Generation for Bit-Vector Programs},
author = {Peisen Yao and Jingyu Ke and Jiahui Sun and Hongfei Fu and Rongxin Wu and Kui Ren},
booktitle = {ASE},
year = {2023},
doi = {10.1109/ase56229.2023.00069}
}