Pang, Jun ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC) ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT)
Lv, Yi
Fan, Dongrui
Cao, Shen
Duan, Kaiqiang
External co-authors :
yes
Language :
English
Title :
paraVerifier: An automatic framework for proving parameterized cache coherence protocols
Publication date :
2015
Event name :
13th International Symposium on Automated Technology for Verification and Analysis
Event date :
2015
Audience :
International
Main work title :
Proceedings of the 13th International Symposium on Automated Technology for Verification and Analysis (ATVA'15)
Pnueli, A., Shahar, E.: A platform for combining deductive with algorithmic verification. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 0302-9743. Springer, Heidelberg (1996)
Björner, N., Browne, A., Manna, Z.: Automatic generation of invariants and intermediate assertions. Theoret. Comput. Sci. 173(1), 49-87 (1997)
Arons, T., Pnueli, A., Ruah, S., Xu, J., Zuck, L.D.: Parameterized verification with automatically computed inductive assertions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 221-234. Springer, Heidelberg (2001)
Pnueli, A., Ruah, S., Zuck, L.D.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 82-97. Springer, Heidelberg (2001)
Tiwari, A., Rues, H., Saïdi, H., Shankar, N.: A technique for invariant generation. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 113-127. Springer, Heidelberg (2001)
Chou, C.-T., Mannava, P.K., Park, S.: A simple method for parameterized verification of cache coherence protocols. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 382-398. Springer, Heidelberg (2004)
Pang, J., Fokkink, W., Hofman, R., Veldema, R.: Model checking a cache coherence protocol of a java DSM implementation. J. Logic Algebraic Program. 71(1), 1-43 (2007)
Pandav, S., Slind, K., Gopalakrishnan, G.C.: Counterexample guided invariant discovery for parameterized cache coherence verification. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 317-331. Springer, Heidelberg (2005)
Lv, Y., Lin, H., Pan, H.: Computing invariants for parameter abstraction. In: Proceedings of the 5th IEEE/ACM Conference on Formal Methods and Models for Codesign (MEMOCODE), pp. 29-38, IEEE CS (2007)
Bingham B.: Automatic non-interference lemmas for parameterized model checking. In: Proceedings of the 8th Conference on Formal Methods in Computer-Aided Design (FMCAD), pp.1-8. IEEE CS (2008)
Conchon, S., Goel, A., Krstić, S., Mebsout, A., Zaïdi, F.: Cubicle: a parallel smtbased model checker for parameterized systems. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 718-724. Springer, Heidelberg (2012)
McMillan, K.L.: Parameterized verification of the FLASH cache coherence protocol by compositional model checking. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 179-195. Springer, Heidelberg (2001)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL - A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)
Park, S., Dill, D.L.: Verification of flash cache coherence protocol by aggregation of distributed transactions. In: Proceedings of the 8th Annual ACM Symposium on Parallel Algorithms and Architectures (SPAA), pp. 288-296. ACM (1996)
Li, Y.: invFinder: An invariant finder (2014). http://lcs.ios.ac.cn/lyj238/invFinder. html
Technical Publications and Training, Intel Corporation: Forte/FL User Guide (2003)
