Parosh Aziz Abdulla, A. Prasad Sistla, and Muralidhar Talupur. 2018. Model Checking Parameterized Systems. In Handbook of Model Checking. 685–725.
Krzysztof R. Apt and Dexter Kozen. 1986. Limits for Automatic Verification of Finite-State Concurrent Systems. Inform. Process. Lett. 22, 6 (1986), 307–309.
Tamarah Arons, Amir Pnueli, Sitvanit Ruah, Jiazhao Xu, and Lenore D. Zuck. 2001. Parameterized Verification with Automatically Computed Inductive Assertions. In Proc. 13th International Conference on Computer Aided Verification (CAV’01) (Lecture Notes in Computer Science, Vol. 2102). Springer, 221–234.
Jialun Cao, Yongjian Li, and Jun Pang. 2018. L-CMP: An automatic learning-based parameterized verification tool (Tool Demo). In Proc. 33rd IEEE/ACM International Conference on Automated Software Engineering (ASE’18). ACM Press, 892–895.
J. Cao, Y. Li, and J. Pang. 2019. A learning-based framework for automatic parameterized verification. In Proc. 37th IEEE International Conference on Computer Design (ICCD’19). IEEE CS, 450–459.
Xiaofang Chen and Ganesh Gopalakrishnan. 2006. A General Compositional Approach to Verifying Hierarchical Cache Coherence Protocols. Technical Report. Technical Report, School of Computing, University of Utah.
Xiaofang Chen, Yu Yang, Ganesh Gopalakrishnan, and Ching-Tsun Chou. 2006. Reducing Verification Complexity of a Multicore Coherence Protocol using Assume/guarantee. In Proc. 6th International Conference on Formal Methods in Computer Aided Design (FMCAD’06). IEEE Computer Society, 81–88.
Ching-Tsun Chou, Phanindra K. Mannava, and Seungjoon Park. 2004. A Simple Method for Parameterized Verification of Cache Coherence Protocols. In Proc. 5th International Conference on Formal Methods in Computer-Aided Design (FMCAD’04) (Lecture Notes in Computer Science, Vol. 3312). Springer, 382–398.
Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. 2003. Counterexample-Guided Abstraction Refinement for Symbolic Model Checking. J. ACM 50, 5 (2003), 752–794.
Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem. 2018. Handbook of Model Checking. Springer.
Ariel Cohen and Kedar S. Namjoshi. 2009. Local Proofs for Global Safety Properties. Formal Methods in System Design 34, 2 (2009), 104–125.
Sylvain Conchon, David Declerck, and Fatiha Zaïdi. 2018. Cubicle-W: Parameterized Model Checking on Weak Memory. In Proc. 9th International Joint Conference on Automated Reasoning (IJCAR’18) (Lecture Notes in Computer Science, Vol. 10900). 152–160.
Sylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout, and Fatiha Zaïdi. 2012. Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems - Tool Paper. In Proc. 24th International Conference on Computer Aided Verification (CAV’12) (Lecture Notes in Computer Science, Vol. 7358). Springer, 718–724.
Sylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout, and Fatiha Zaïdi. 2013. Invariants for Finite Instances and Beyond. In Proc. 13th International Conference on Formal Methods in Computer-Aided Design (FMCAD’13). IEEE Computer Society, 61–68.
David L. Dill. 1996. The Murphi Verification System. In Proc. 8th International Conference on Computer Aided Verification (CAV’96) (Lecture Notes in Computer Science, Vol. 1102). Springer, 390–393.
Michael Emmi, Rupak Majumdar, and Roman Manevich. 2010. Parameterized Verification of Transactional Memories. In Proc. 31th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’10). ACM Press, 134–145.
Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, and Jan-Georg Smaus. 2013. A Fully Verified Executable LTL Model Checker. In Proc. 25th International Conference on Computer Aided Verification (CAV’13) (Lecture Notes in Computer Science, Vol. 8044). Springer, 463–478.
Jochen Hoenicke, Rupak Majumdar, and Andreas Podelski. 2017. Thread Modularity at Many Levels: A Pearl in Compositional Verification. In Proc. 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL’17). ACM Press, 473–485.
Peter Huber, Arne M. Jensen, Leif O. Jepsen, and Kurt Jensen. 1984. Towards Reachability Trees for High-level Petri Nets. In Proc. 6th European Workshop on Applications and Theory in Petri Nets (Lecture Notes in Computer Science, Vol. 188). Springer, 215–233.
C. Norris Ip and David L. Dill. 1993. Efficient Verification of Symmetric Concurrent Systems. In Proc. International Conference on Computer Design (ICCD’93). IEEE Computer Soceity, 230–234.
C. Norris Ip and David L. Dill. 1996. Better Verification through Symmetry. Formal Methods in System Design 9, 1/2 (1996), 41–75.
Sava Krstic. 2005. Parameterized System Verification with Guard Strengthening and Parameter Abstraction. Proc. 4th Workshop on Automated Verification of Infinite State Systems (AVIS’05) (2005).
Shuvendu K. Lahiri and Randal E. Bryant. 2004. Constructing Quantified Invariants via Predicate Abstraction. In Proc. 5th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’04) (Lecture Notes in Computer Science, Vol. 2937). Springer, 267–281.
Yongjian Li, Kaiqiang Duan, Yi Lv, Jun Pang, and Shaowei Cai. 2016. A Novel Approach to Parameterized Verification of Cache Coherence Protocols. In Proc. 34th IEEE International Conference on Computer Design (ICCD’16). IEEE Computer Society, 560–567.
Yongjian Li and Zimin Li. 2022. ILCMP source code. https://gitee.com/dust_capacity_i/ILCMP.git
Yongjian Li, Zimin Li, Bohua Zhan, and Jun Pang. 2023. autoCMP. https://github.com/forSubmission238/autoCMP.
Kenneth L. McMillan. 1999. Verification of Infinite State Systems by Compositional Model Checking. In Proc. 10th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME’99) (Lecture Notes in Computer Science, Vol. 1703). Springer, 219–234.
Kenneth L. McMillan. 2001. Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking. In Proc. 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME’01) (Lecture Notes in Computer Science, Vol. 2144). Springer, 179–195.
Kenneth L. McMillan. 2008. Quantified Invariant Generation using An Interpolating Saturation Prover. In Proc. 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’08) (Lecture Notes in Computer Science, Vol. 4963). Springer, 413–427.
Kenneth L. McMillan. 2016. Modular Specification and Verification of a Cache-coherent Interface. In Proc. 16th International Conference on Formal Methods in Computer-Aided Design (FMCAD’16). IEEE, 109–116.
Kenneth L. McMillan. 2018. Eager Abstraction for Symbolic Model Checking. In Proc. 30th International Conference on Computer Aided Verification (CAV’18) (Lecture Notes in Computer Science, Vol. 10981). Springer, 191–208.
Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2002. Isabelle/HOL - A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, Vol. 2283. Springer.
Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, and Sharon Shoham. 2016. Ivy: Safety Verification by Interactive Generalization. In Proc. 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’18). ACM Press, 614–630.
Sudhindra Pandav, Konrad Slind, and Ganesh Gopalakrishnan. 2005. Counterexample Guided Invariant Discovery for Parameterized Cache Coherence Verification. In Proc. 13th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME’05) (Lecture Notes in Computer Science, Vol. 3725). Springer, 317–331.
Seungjoon Park and David L Dill. 1996. Verification of FLASH Cache Coherence Protocol by Aggregation of Distributed Transactions. In Proc. 8th ACM Symposium on Parallel Algorithms and Architectures (SPAA’96). ACM, 288–296.
Amir Pnueli, Sitvanit Ruah, and Lenore D. Zuck. 2001. Automatic Deductive Verification with Invisible Invariants. In Proc. 7th International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS’01) (Lecture Notes in Computer Science, Vol. 2031). Springer, 82–97.
Amir Pnueli and Elad Shahar. 1996. A Platform for Combining Deductive with Algorithmic Verification. In Proc. 8th International Conference on Computer Aided Verification (CAV’96) (Lecture Notes in Computer Science, Vol. 1102). Springer, 184–195.
Peter H Starke. 1991. Reachability analysis of Petri Nets using Symmetries. Systems Analysis Modelling Simulation 8, 4-5 (1991), 293–303.
Murali Talupur and Mark R. Tuttle. 2008. Going with the Flow: Parameterized Verification using Message Flows. In Proc. 8th International Conference on Formal Methods in Computer-Aided Design (FMCAD’08). IEEE Computer Society, 1–8.
Marcelo Taube, Giuliano Losa, Kenneth L. McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R. Wilcox, and Doug Woos. 2018. Modularity for Decidability of Deductive Verification with Applications to Distributed Systems. In Proc. 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’18). ACM Press, 662–677.
Ashish Tiwari, Harald Rueß, Hassen Saïdi, and Natarajan Shankar. 2001. A Technique for Invariant Generation. In Proc. 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’01) (Lecture Notes in Computer Science, Vol. 2031). Springer, 113–127.
Pierre Wolper. 1986. Expressing Interesting Properties of Programs in Propositional Temporal Logic. In Proc. 13th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL’86). ACM Press, 184–193.
Pierre Wolper and Vinciane Lovinfosse. 1989. Verifying Properties of Large Sets of Processes with Network Invariants. In Proc. 1st International Conference on Computer Aided Verification (CAV’89) (Lecture Notes in Computer Science, Vol. 407). Springer, 60–80.
