{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:32:43Z","timestamp":1750221163432,"version":"3.41.0"},"reference-count":32,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2018,10,31]],"date-time":"2018-10-31T00:00:00Z","timestamp":1540944000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61672503, 61532019,61761136011,61472473"],"award-info":[{"award-number":["61672503, 61532019,61761136011,61472473"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002855","name":"Ministry of Science and Technology of the People's Republic of China","doi-asserted-by":"publisher","award":["2017YFB0801900"],"award-info":[{"award-number":["2017YFB0801900"]}],"id":[{"id":"10.13039\/501100002855","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2018,10,31]]},"abstract":"<jats:p>Formal verification of parameterized protocols such as cache coherence protocols is a significant challenge. In this article, we propose an automatic proving approach and its prototype paraVerifier to handle this challenge within a unified framework as follows: (1) To prove the correctness of a parameterized protocol, our approach automatically discovers auxiliary invariants and the corresponding dependency relations among the discovered invariants and protocol rules from a small instance of the to-be-verified protocol, and (2) the discovered invariants and dependency graph are then automatically generalized into a parameterized form and sent to the theorem prover, Isabelle. As a side product, the final verification result of a protocol is provided by a formal and human-readable proof. Our approach has been successfully applied to a number of benchmarks, including snoopying-based and directory-based cache coherence protocols.<\/jats:p>","DOI":"10.1145\/3232164","type":"journal-article","created":{"date-parts":[[2018,12,4]],"date-time":"2018-12-04T13:14:12Z","timestamp":1543929252000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["An Automatic Proving Approach to Parameterized Verification"],"prefix":"10.1145","volume":"19","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2589-3648","authenticated-orcid":false,"given":"Yongjian","family":"Li","sequence":"first","affiliation":[{"name":"State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kaiqiang","family":"Duan","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David N.","family":"Jansen","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jun","family":"Pang","sequence":"additional","affiliation":[{"name":"Faculty of Science, Technology and Communication and Interdisciplinary Centre for Security, Reliability and Trust, University of Luxembourg, Luxembourg"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lijun","family":"Zhang","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Computer Science, Institute of Software, University of Chinese Academy of Sciences, Chinese Academy of Sciences, Beijing, P.R.China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yi","family":"Lv","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Computer Science, Institute of Software, University of Chinese Academy of Sciences, Chinese Academy of Sciences, Beijing, P.R.China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shaowei","family":"Cai","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Computer Science, Institute of Software, University of Chinese Academy of Sciences, Chinese Academy of Sciences, Beijing, P.R.China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2018,11,30]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_2_1_1_1","DOI":"10.1007\/978-3-642-35873-9_28"},{"volume-title":"AMD64 Architecture Programmer\u2019s Manual","unstructured":"AMD64 Technology. 2013. AMD64 Architecture Programmer\u2019s Manual . Vol. 2 . Advanced Micro Devices , {s. l.}. AMD64 Technology. 2013. AMD64 Architecture Programmer\u2019s Manual. Vol. 2. Advanced Micro Devices, {s. l.}.","key":"e_1_2_1_2_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_3_1","DOI":"10.5555\/647770.734120"},{"volume-title":"Principles of Model Checking","author":"Baier Christel","unstructured":"Christel Baier and Joost-Pieter Katoen . 2008. Principles of Model Checking . MIT Press , Cambridge, MA . Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. MIT Press, Cambridge, MA.","key":"e_1_2_1_4_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_5_1","DOI":"10.5555\/646541.696180"},{"doi-asserted-by":"publisher","key":"e_1_2_1_6_1","DOI":"10.1016\/S0304-3975(96)00191-0"},{"doi-asserted-by":"publisher","key":"e_1_2_1_7_1","DOI":"10.1145\/2951860.2951873"},{"doi-asserted-by":"publisher","key":"e_1_2_1_8_1","DOI":"10.1007\/978-3-540-30494-4_27"},{"unstructured":"Edmund M. Clarke Orna Grumberg and Doron Peled. 1999. Model Checking. MIT Press Cambridge MA.   Edmund M. Clarke Orna Grumberg and Doron Peled. 1999. Model Checking. MIT Press Cambridge MA.","key":"e_1_2_1_9_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_10_1","DOI":"10.1007\/978-3-642-31424-7_55"},{"doi-asserted-by":"publisher","key":"e_1_2_1_11_1","DOI":"10.1109\/FMCAD.2013.6679392"},{"volume-title":"Formal Methods: FM (LNCS), Nikolaj Bj\u00f8rner and Frank de Boer (Eds.)","author":"Conchon Sylvain","unstructured":"Sylvain Conchon , Alain Mebsout , and Fatiha Za\u00efdi . 2015. Certificates for parameterized model checking . In Formal Methods: FM (LNCS), Nikolaj Bj\u00f8rner and Frank de Boer (Eds.) , Vol. 9109 . Springer , Cham , 126--142. Sylvain Conchon, Alain Mebsout, and Fatiha Za\u00efdi. 2015. Certificates for parameterized model checking. In Formal Methods: FM (LNCS), Nikolaj Bj\u00f8rner and Frank de Boer (Eds.), Vol. 9109. Springer, Cham, 126--142.","key":"e_1_2_1_12_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_13_1","DOI":"10.1007\/978-3-319-41528-4_16"},{"doi-asserted-by":"publisher","key":"e_1_2_1_14_1","DOI":"10.1007\/978-3-540-39724-3_22"},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design. IEEE.","author":"German Steven M.","year":"2004","unstructured":"Steven M. German . 2004 . Tutorial on verification of distributed cache memory protocols . In Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design. IEEE. Steven M. German. 2004. Tutorial on verification of distributed cache memory protocols. In Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design. IEEE."},{"doi-asserted-by":"publisher","key":"e_1_2_1_16_1","DOI":"10.1007\/978-3-540-71070-7_6"},{"key":"e_1_2_1_17_1","volume-title":"Article 10","author":"Ghilardi Silvio","year":"2010","unstructured":"Silvio Ghilardi and Silvio Ranise . 2010. Backward reachability of array-based systems by SMT solving: Termination and invariant synthesis. Logic. Methods Comput. Sci. 6, 4 , Article 10 ( 2010 ), 48 pages. Silvio Ghilardi and Silvio Ranise. 2010. Backward reachability of array-based systems by SMT solving: Termination and invariant synthesis. Logic. Methods Comput. Sci. 6, 4, Article 10 (2010), 48 pages."},{"doi-asserted-by":"publisher","key":"e_1_2_1_18_1","DOI":"10.1007\/978-3-642-14295-6_55"},{"doi-asserted-by":"publisher","key":"e_1_2_1_19_1","DOI":"10.1145\/191995.192056"},{"unstructured":"Y. Li and K. Duan. 2016. The software tool ParaVerifier. Retrieved from https:\/\/github.com\/paraVerifier\/paraVerifier.  Y. Li and K. Duan. 2016. The software tool ParaVerifier. Retrieved from https:\/\/github.com\/paraVerifier\/paraVerifier.","key":"e_1_2_1_20_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_21_1","DOI":"10.1109\/ICCD.2016.7753341"},{"doi-asserted-by":"publisher","key":"e_1_2_1_22_1","DOI":"10.1007\/978-3-319-24953-7_15"},{"doi-asserted-by":"publisher","key":"e_1_2_1_23_1","DOI":"10.1109\/MEMCOD.2007.371252"},{"doi-asserted-by":"publisher","key":"e_1_2_1_24_1","DOI":"10.5555\/646705.702177"},{"volume-title":"A Proof Assistant for Higher-Order Logic. LNCS","author":"Nipkow Tobias","unstructured":"Tobias Nipkow , Lawrence C. Paulson , and Markus Wenzel . 2002. Isabelle\/HOL : A Proof Assistant for Higher-Order Logic. LNCS , Vol. 2283 . Springer , Berlin . Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2002. Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS, Vol. 2283. Springer, Berlin.","key":"e_1_2_1_25_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_26_1","DOI":"10.1007\/11560548_24"},{"doi-asserted-by":"publisher","key":"e_1_2_1_27_1","DOI":"10.1145\/773453.808204"},{"doi-asserted-by":"publisher","key":"e_1_2_1_28_1","DOI":"10.1145\/237502.237573"},{"doi-asserted-by":"publisher","key":"e_1_2_1_29_1","DOI":"10.5555\/646485.694452"},{"doi-asserted-by":"publisher","key":"e_1_2_1_30_1","DOI":"10.5555\/647765.735986"},{"volume-title":"Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201908)","author":"Talupur Murali","unstructured":"Murali Talupur and Mark R. Tuttle . 2008. Going with the flow: Parameterized verification using message flows . In Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201908) . IEEE Press, 10:1--10:8. Murali Talupur and Mark R. Tuttle. 2008. Going with the flow: Parameterized verification using message flows. In Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201908). IEEE Press, 10:1--10:8.","key":"e_1_2_1_31_1"},{"key":"e_1_2_1_32_1","volume-title":"Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201901)","volume":"2031","author":"Tiwari A.","unstructured":"A. Tiwari , H. Rue\u00df , H. Sa\u00efdi , and N. Shankar . 2001. A technique for invariant generation . In Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201901) , Tiziana Margaria and Wang Yi (Eds.), LNCS , Vol. 2031 . Springer, Berlin, 113--127. A. Tiwari, H. Rue\u00df, H. Sa\u00efdi, and N. Shankar. 2001. A technique for invariant generation. In Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201901), Tiziana Margaria and Wang Yi (Eds.), LNCS, Vol. 2031. Springer, Berlin, 113--127."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3232164","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3232164","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:08:46Z","timestamp":1750208926000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3232164"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,10,31]]},"references-count":32,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2018,10,31]]}},"alternative-id":["10.1145\/3232164"],"URL":"https:\/\/doi.org\/10.1145\/3232164","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2018,10,31]]},"assertion":[{"value":"2017-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-06-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-11-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}