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

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.