paperbot · PL 论文追踪

全部论文 待读 收藏

P2 L-CMP: an automatic learning-based parameterized verification tool

L-CMP：一种基于学习的自动参数化验证工具
ASE Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering2018匹配度 4/10 · 论文属于机器学习辅助形式化验证，与AI→PL方向有交集，且包含工业级协议验证的工具实现；但使用的是传统学习与模型检测，不涉及用户重点关注的LLM/Agent、浮点程序分析或贝叶斯程序分析，研究场景也非ML系统/Agentic程序。引用 1 inbox
Jialun Cao, Yongjian Li, Jun Pang
程序验证机器学习与程序语言
crossref: 2026-09-12

AI 速览

一句话：提出基于学习的参数化验证工具 L-CMP，自动学习可读辅助不变式并结合模型检测验证协议。

本文介绍 L-CMP，一个自动的、基于学习的参数化验证工具。参数化协议由于进程数量任意，直接验证通常十分困难；L-CMP 将机器学习与模型检测技术相结合，针对给定参数化协议自动学习一组辅助不变式，并利用这些不变式完成协议验证。其学习到的不变式具有直观、可读的特点，便于理解验证依据。实验结果表明，L-CMP 能够成功验证多个缓存一致性协议，包括工业规模的 FLASH 协议。该工作展示了学习不变式与模型检测结合在参数化验证中的有效性，并提供了可下载工具与演示视频。

问题
参数化协议中进程数量任意，导致状态空间无限，传统模型检测难以直接自动验证。
方法
L-CMP 结合机器学习与模型检测，自动为参数化协议学习一组直观可读的辅助不变式，并基于这些不变式实现自动验证。
评估
在多个缓存一致性协议上进行实验，包括工业规模的 FLASH 协议，结果表明工具可成功完成验证。
原文摘要（Abstract）

This demo introduces L-CMP, an automatic learning-based parameterized verification tool. It can verify parameterized protocols by combining machine learning and model checking techniques. Given a parameterized protocol, L-CMP learns a set of auxiliary invariants and implements verification of the protocol using the invariants automatically. In particular, the learned auxiliary invariants are straightforward and readable. The experimental results show that L-CMP can successfully verify a number of cache coherence protocols, including the industrial-scale FLASH protocol. The video is available at https://youtu.be/6Dl2HiiiS4E, and L-CMPL-CMP can be downloaded at https://github.com/ ArabelaTso/Learning-Based-ParaVerifer.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@inproceedings{paperbot4706,
  title = {L-CMP: an automatic learning-based parameterized verification tool},
  author = {Jialun Cao and Yongjian Li and Jun Pang},
  booktitle = {ASE},
  year = {2018},
  doi = {10.1145/3238147.3240487}
}