{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T18:19:07Z","timestamp":1784830747045,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642279393","type":"print"},{"value":"9783642279409","type":"electronic"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-27940-9_23","type":"book-chapter","created":{"date-parts":[[2012,1,19]],"date-time":"2012-01-19T02:29:29Z","timestamp":1326940169000},"page":"348-362","source":"Crossref","is-referenced-by-count":11,"title":["Local Symmetry and Compositional Verification"],"prefix":"10.1007","author":[{"given":"Kedar S.","family":"Namjoshi","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Richard J.","family":"Trefler","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"23_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/3-540-36135-9_15","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2002","author":"N. Amla","year":"2002","unstructured":"Amla, N., Emerson, E.A., Namjoshi, K.S., Trefler, R.J.: Visual Specifications for Modular Reasoning About Asynchronous Systems. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol.\u00a02529, pp. 226\u2013242. Springer, Heidelberg (2002)"},{"key":"23_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/3-540-44585-4_19","volume-title":"Computer Aided Verification","author":"T. Arons","year":"2001","unstructured":"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.\u00a02102, pp. 221\u2013234. Springer, Heidelberg (2001)"},{"key":"23_CR3","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1112\/blms\/19.2.113","volume":"19","author":"R. Brown","year":"1987","unstructured":"Brown, R.: From groups to groupoids: A brief survey. Bull. London Math. Society\u00a019, 113\u2013134 (1987)","journal-title":"Bull. London Math. Society"},{"key":"23_CR4","doi-asserted-by":"crossref","unstructured":"Chandy, K., Misra, J.: Proofs of networks of processes. IEEE Transactions on Software Engineering\u00a07(4) (1981)","DOI":"10.1109\/TSE.1981.230844"},{"issue":"12","key":"23_CR5","doi-asserted-by":"publisher","first-page":"1465","DOI":"10.1109\/43.552080","volume":"15","author":"H. Cho","year":"1996","unstructured":"Cho, H., Hachtel, G.D., Macii, E., Plessier, B., Somenzi, F.: Algorithms for approximate FSM traversal based on state space decomposition. IEEE Trans. on CAD of Integrated Circuits and Systems\u00a015(12), 1465\u20131478 (1996)","journal-title":"IEEE Trans. on CAD of Integrated Circuits and Systems"},{"key":"23_CR6","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Filkorn, T., Jha, S.: Exploiting Symmetry in Temporal Logic Model Checking. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697. Springer, Heidelberg (1993)","DOI":"10.1007\/3-540-56922-7_37"},{"key":"23_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/3-540-36577-X_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.M. Cobleigh","year":"2003","unstructured":"Cobleigh, J.M., Giannakopoulou, D., P\u0103s\u0103reanu, C.S.: Learning Assumptions for Compositional Verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 331\u2013346. Springer, Heidelberg (2003)"},{"key":"23_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-540-73368-3_9","volume-title":"Computer Aided Verification","author":"A. Cohen","year":"2007","unstructured":"Cohen, A., Namjoshi, K.S.: Local Proofs for Global Safety Properties. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 55\u201367. Springer, Heidelberg (2007)"},{"key":"23_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-540-70545-1_15","volume-title":"Computer Aided Verification","author":"A. Cohen","year":"2008","unstructured":"Cohen, A., Namjoshi, K.S.: Local Proofs for Linear-Time Properties of Concurrent Programs. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 149\u2013161. Springer, Heidelberg (2008)"},{"issue":"2","key":"23_CR10","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/s10703-008-0063-8","volume":"34","author":"A. Cohen","year":"2009","unstructured":"Cohen, A., Namjoshi, K.S.: Local proofs for global safety properties. Formal Methods in System Design\u00a034(2), 104\u2013125 (2009)","journal-title":"Formal Methods in System Design"},{"key":"23_CR11","unstructured":"de Roever, W.-P., de Boer, F., Hannemann, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification: Introduction to Compositional and Noncompositional Proof Methods. Cambridge University Press (2001)"},{"key":"23_CR12","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-3228-5","volume-title":"Predicate Calculus and Program Semantics","author":"E. Dijkstra","year":"1990","unstructured":"Dijkstra, E., Scholten, C.: Predicate Calculus and Program Semantics. Springer, Heidelberg (1990)"},{"key":"23_CR13","doi-asserted-by":"crossref","unstructured":"Emerson, E., Namjoshi, K.: Reasoning about rings. In: ACM Symposium on Principles of Programming Languages (1995)","DOI":"10.1145\/199448.199468"},{"key":"23_CR14","doi-asserted-by":"crossref","unstructured":"Emerson, E., Sistla, A.: Symmetry and Model Checking. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697. Springer, Heidelberg (1993)","DOI":"10.1007\/3-540-56922-7_38"},{"key":"23_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-44829-2_14","volume-title":"Model Checking Software","author":"C. Flanagan","year":"2003","unstructured":"Flanagan, C., Qadeer, S.: Thread-Modular Model Checking. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 213\u2013224. Springer, Heidelberg (2003)"},{"key":"23_CR16","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1090\/S0273-0979-06-01108-6","volume":"43","author":"M. Golubitsky","year":"2006","unstructured":"Golubitsky, M., Stewart, I.: Nonlinear dynamics of networks: the groupoid formalism. Bull. Amer. Math. Soc.\u00a043, 305\u2013364 (2006)","journal-title":"Bull. Amer. Math. Soc."},{"key":"23_CR17","doi-asserted-by":"crossref","unstructured":"Gupta, A., Popeea, C., Rybalchenko, A.: Predicate abstraction and refinement for verifying multi-threaded programs. In: POPL. ACM (2011)","DOI":"10.1145\/1926385.1926424"},{"key":"23_CR18","doi-asserted-by":"crossref","unstructured":"Ip, C.N., Dill, D.: Better verification through symmetry. Formal Methods in System Design\u00a09(1\/2) (1996)","DOI":"10.1007\/BF00625968"},{"key":"23_CR19","doi-asserted-by":"crossref","unstructured":"Jones, C.: Tentative steps toward a development method for interfering programs. ACM Trans. on Programming Languages and Systems, TOPLAS (1983)","DOI":"10.1145\/69575.69577"},{"key":"23_CR20","doi-asserted-by":"crossref","unstructured":"Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Software Eng.\u00a03(2) (1977)","DOI":"10.1109\/TSE.1977.229904"},{"issue":"2","key":"23_CR21","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1145\/2993.357247","volume":"6","author":"L. Lamport","year":"1984","unstructured":"Lamport, L., Schneider, F.B.: The \u201cHoare Logic\u201d of CSP, and All That. ACM Trans. Program. Lang. Syst.\u00a06(2), 281\u2013296 (1984)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"23_CR22","unstructured":"Moon, I.-H., Kukula, J.H., Shiple, T.R., Somenzi, F.: Least fixpoint approximations for reachability analysis. In: ICCAD, pp. 41\u201344 (1999)"},{"key":"23_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-540-69738-1_22","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"K.S. Namjoshi","year":"2007","unstructured":"Namjoshi, K.S.: Symmetry and Completeness in the Analysis of Parameterized Systems. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 299\u2013313. Springer, Heidelberg (2007)"},{"key":"23_CR24","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1740582.1740584","volume":"11","author":"K.S. Namjoshi","year":"2010","unstructured":"Namjoshi, K.S., Trefler, R.J.: On the completeness of compositional reasoning methods. ACM Trans. Comput. Logic\u00a011, 16:1\u201316:22 (2010)","journal-title":"ACM Trans. Comput. Logic"},{"issue":"5","key":"23_CR25","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1145\/360051.360224","volume":"19","author":"S.S. Owicki","year":"1976","unstructured":"Owicki, S.S., Gries, D.: Verifying properties of parallel programs: An axiomatic approach. Commun. ACM\u00a019(5), 279\u2013285 (1976)","journal-title":"Commun. ACM"},{"key":"23_CR26","unstructured":"Weinstein, A.: Groupoids: Unifying internal and external symmetry-a tour through some examples. Notices of the AMS (1996)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-27940-9_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,24]],"date-time":"2019-04-24T22:51:10Z","timestamp":1556146270000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-27940-9_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642279393","9783642279409"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-27940-9_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}