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

Jialun Cao; Yongjian Li; Jun Pang

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

Jialun Cao, Yongjian Li^*, Jun Pang

^*Corresponding author for this work

Research output: Chapter in Book/Conference Proceeding/Report › Conference Paper published in a book › peer-review

2 Citations (Scopus)

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 presentation of L-CMP is available at https://youtu.be/6Dl2HiiiS4E, and the source code can be downloaded at https://github.com/ArabelaTso/Learning-Based-ParaVerifer.

Original language	English
Title of host publication	ASE 2018 - Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering
Editors	Christian Kastner, Marianne Huchard, Gordon Fraser
Publisher	Association for Computing Machinery, Inc
Pages	892-895
Number of pages	4
ISBN (Electronic)	9781450359375
Publication status	Published - 3 Sept 2018
Externally published	Yes
Event	33rd IEEE/ACM International Conference on Automated Software Engineering, ASE 2018 - Montpellier, France Duration: 3 Sept 2018 → 7 Sept 2018

Publication series

Name	ASE 2018 - Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering

Conference

Conference	33rd IEEE/ACM International Conference on Automated Software Engineering, ASE 2018
Country/Territory	France
City	Montpellier
Period	3/09/18 → 7/09/18

Bibliographical note

Publisher Copyright:
© 2018 Copyright held by the owner/author(s). Publication rights licensed to ACM.

Keywords

Association rule learning
Machine learning
Model checking
Parameterized verification

Access to Document

https://hdl.handle.net/1783.1/141470

Cite this

Cao, J., Li, Y., & Pang, J. (2018). L-CMP: An automatic learning-based parameterized verification tool. In C. Kastner, M. Huchard, & G. Fraser (Eds.), ASE 2018 - Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering (pp. 892-895). (ASE 2018 - Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering). Association for Computing Machinery, Inc. https://hdl.handle.net/1783.1/141470

Cao, Jialun ; Li, Yongjian ; Pang, Jun. / L-CMP : An automatic learning-based parameterized verification tool. ASE 2018 - Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering. editor / Christian Kastner ; Marianne Huchard ; Gordon Fraser. Association for Computing Machinery, Inc, 2018. pp. 892-895 (ASE 2018 - Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering).

@inproceedings{05289993f16045babe8132e3053a6349,

title = "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 presentation of L-CMP is available at https://youtu.be/6Dl2HiiiS4E, and the source code can be downloaded at https://github.com/ArabelaTso/Learning-Based-ParaVerifer.",

keywords = "Association rule learning, Machine learning, Model checking, Parameterized verification",

author = "Jialun Cao and Yongjian Li and Jun Pang",

note = "Publisher Copyright: {\textcopyright} 2018 Copyright held by the owner/author(s). Publication rights licensed to ACM.; 33rd IEEE/ACM International Conference on Automated Software Engineering, ASE 2018 ; Conference date: 03-09-2018 Through 07-09-2018",

year = "2018",

month = sep,

day = "3",

language = "English",

series = "ASE 2018 - Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering",

publisher = "Association for Computing Machinery, Inc",

pages = "892--895",

editor = "Christian Kastner and Marianne Huchard and Gordon Fraser",

booktitle = "ASE 2018 - Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering",

}

Cao, J, Li, Y & Pang, J 2018, L-CMP: An automatic learning-based parameterized verification tool. in C Kastner, M Huchard & G Fraser (eds), ASE 2018 - Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering. ASE 2018 - Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, Association for Computing Machinery, Inc, pp. 892-895, 33rd IEEE/ACM International Conference on Automated Software Engineering, ASE 2018, Montpellier, France, 3/09/18. <https://hdl.handle.net/1783.1/141470>

L-CMP: An automatic learning-based parameterized verification tool. / Cao, Jialun; Li, Yongjian; Pang, Jun.
ASE 2018 - Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering. ed. / Christian Kastner; Marianne Huchard; Gordon Fraser. Association for Computing Machinery, Inc, 2018. p. 892-895 (ASE 2018 - Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering).

Research output: Chapter in Book/Conference Proceeding/Report › Conference Paper published in a book › peer-review

TY - GEN

T1 - L-CMP

T2 - 33rd IEEE/ACM International Conference on Automated Software Engineering, ASE 2018

AU - Cao, Jialun

AU - Li, Yongjian

AU - Pang, Jun

PY - 2018/9/3

Y1 - 2018/9/3

N2 - 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 presentation of L-CMP is available at https://youtu.be/6Dl2HiiiS4E, and the source code can be downloaded at https://github.com/ArabelaTso/Learning-Based-ParaVerifer.

AB - 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 presentation of L-CMP is available at https://youtu.be/6Dl2HiiiS4E, and the source code can be downloaded at https://github.com/ArabelaTso/Learning-Based-ParaVerifer.

KW - Association rule learning

KW - Machine learning

KW - Model checking

KW - Parameterized verification

UR - https://www.scopus.com/pages/publications/85056546740

M3 - Conference Paper published in a book

AN - SCOPUS:85056546740

T3 - ASE 2018 - Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering

SP - 892

EP - 895

BT - ASE 2018 - Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering

A2 - Kastner, Christian

A2 - Huchard, Marianne

A2 - Fraser, Gordon

PB - Association for Computing Machinery, Inc

Y2 - 3 September 2018 through 7 September 2018

ER -

Cao J, Li Y, Pang J. L-CMP: An automatic learning-based parameterized verification tool. In Kastner C, Huchard M, Fraser G, editors, ASE 2018 - Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering. Association for Computing Machinery, Inc. 2018. p. 892-895. (ASE 2018 - Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering).

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

Abstract

Publication series

Conference

Bibliographical note

Keywords

Access to Document

Other files and links

Fingerprint

Cite this