{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T13:14:15Z","timestamp":1742390055594},"publisher-location":"Berlin, Heidelberg","reference-count":41,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540677703"},{"type":"electronic","value":"9783540450474"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10722167_33","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T22:00:33Z","timestamp":1167429633000},"page":"435-449","source":"Crossref","is-referenced-by-count":42,"title":["Syntactic Program Transformations for Automatic Abstraction"],"prefix":"10.1007","author":[{"given":"Kedar S.","family":"Namjoshi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert P.","family":"Kurshan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"33_CR1","doi-asserted-by":"crossref","unstructured":"Browne, M.C., Clarke, E.M., Gr\u00fcmberg, O.: Characterizing finite Kripke structures in Propositional Temporal Logic. Theoretical Computer Science\u00a059 (1988)","DOI":"10.21236\/ADA188620"},{"key":"33_CR2","doi-asserted-by":"crossref","unstructured":"Bohn, J., Damm, W., Grumberg, O., Hungar, H., Laster, K.: First- order-CTL model checking. In: Arvind, V., Sarukkai, S. (eds.) FST TCS 1998. LNCS, vol.\u00a01530. Springer, Heidelberg (1998)","DOI":"10.1007\/978-3-540-49382-2_27"},{"key":"#cr-split#-33_CR3.1","unstructured":"Bouajjani, A., Fernandez, J.-C., Halbwachs, N.: Minimal model generation. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol.??663. Springer, Heidelberg (1993);"},{"key":"#cr-split#-33_CR3.2","unstructured":"Full version in Science of Computer Programming 18 (1992)"},{"key":"33_CR4","doi-asserted-by":"crossref","unstructured":"Bultan, T., Gerber, R., Pugh, W.: Symbolic model checking of infinite state systems using Presburger arithmetic. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254. Springer, Heidelberg (1997)","DOI":"10.1007\/3-540-63166-6_39"},{"key":"33_CR5","doi-asserted-by":"crossref","unstructured":"Bensalem, S., Lakhnech, Y., Owre, S.: Computing abstractions of infinite state systems compositionally and automatically. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427. Springer, Heidelberg (1998)","DOI":"10.1007\/BFb0028755"},{"key":"33_CR6","doi-asserted-by":"crossref","unstructured":"Chan, W., Anderson, R., Beame, P., Notkin, D.: Combining constraint solving and symbolic model checking for a class of systems with non-linear constraints. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254. Springer, Heidelberg (1997)","DOI":"10.1007\/3-540-63166-6_32"},{"key":"33_CR7","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Workshop on Logics of Programs. LNCS, vol.\u00a0131. Springer, Hidelberg (1981)"},{"key":"33_CR8","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic. TOPLAS\u00a08(2) (1986)","DOI":"10.1145\/5397.5399"},{"key":"33_CR9","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":"33_CR10","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Long, D.: Model checking and abstraction. TOPLAS (1994)","DOI":"10.1145\/186025.186051"},{"key":"33_CR11","doi-asserted-by":"crossref","unstructured":"Colon, M.A., Uribe, T.E.: Generating finite-state abstractions of reactive systems using decision procedures. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427. Springer, Heidelberg (1998)","DOI":"10.1007\/BFb0028753"},{"key":"33_CR12","doi-asserted-by":"crossref","unstructured":"Dams, D., Gerth, R., Grumberg, O.: Generation of reduced models for checking fragments of CTL. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697. Springer, Heidelberg (1993)","DOI":"10.1007\/3-540-56922-7_39"},{"key":"33_CR13","doi-asserted-by":"crossref","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy, and formal deriva- tion of programs. C. ACM 18 (1975)","DOI":"10.1145\/800027.808417"},{"key":"33_CR14","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Halpern, J.: \u201cSometimes\u201d and \u201cNot Never\u201d revisited: On branching versus linear time temporal logic. J. ACM\u00a033 (1986)","DOI":"10.1145\/4904.4999"},{"key":"33_CR15","unstructured":"Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional mu-calculus (extended abstract). In: LICS (1986)"},{"key":"33_CR16","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Sistla, A.P.: 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":"33_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/3-540-48153-2_12","volume-title":"Correct Hardware Design and Verification Methods","author":"E.A. Emerson","year":"1999","unstructured":"Emerson, E.A., Trefler, R.J.: From asymmetry to full symmetry: New techniques for symmetry reduction in model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 142\u2013157. Springer, Heidelberg (1999)"},{"key":"33_CR18","doi-asserted-by":"crossref","unstructured":"Grumberg, O., Long, D.: Model checking and modular verification. TOPLAS\u00a016 (1994)","DOI":"10.1145\/177492.177725"},{"key":"33_CR19","doi-asserted-by":"crossref","unstructured":"German, S., Sistla, A.P.: Reasoning about systems with many processes. J. ACM (1992)","DOI":"10.1145\/146637.146681"},{"key":"33_CR20","doi-asserted-by":"crossref","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254. Springer, Heidelberg (1997)","DOI":"10.1007\/3-540-63166-6_10"},{"key":"33_CR21","doi-asserted-by":"crossref","unstructured":"Hojati, R., Brayton, R.K.: Automatic datapath abstraction of hardware systems. In: Wolper, P. (ed.) CAV 1995. LNCS, vol.\u00a0939. Springer, Heidelberg (1995)","DOI":"10.1007\/3-540-60045-0_43"},{"key":"33_CR22","doi-asserted-by":"crossref","unstructured":"Hungar, H., Grumberg, O., Damm, W.: What if model checking must be truly symbolic. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol.\u00a0987. Springer, Heidelberg (1995)","DOI":"10.1007\/3-540-60385-9_1"},{"key":"33_CR23","doi-asserted-by":"crossref","unstructured":"Henzinger, M.R., Henzinger, T.A., Kopke, P.W.: Computing simulations on finite and infinite graphs. In: IEEE FOCS (1995)","DOI":"10.1109\/SFCS.1995.492576"},{"key":"33_CR24","unstructured":"Ip, C.N., Dill, D.L.: Better verification through symmetry. Formal Methods in System Design (1996)"},{"key":"33_CR25","doi-asserted-by":"crossref","unstructured":"Keller, R.M.: Formal verification of parallel programs. C. ACM (1976)","DOI":"10.1145\/360248.360251"},{"key":"33_CR26","doi-asserted-by":"crossref","unstructured":"Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic model checking with rich assertional languages. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254. Springer, Heidelberg (1997)","DOI":"10.1007\/3-540-63166-6_41"},{"key":"33_CR27","doi-asserted-by":"crossref","unstructured":"Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic model checking with rich assertional languages. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254. Springer, Heidelberg (1997)","DOI":"10.1007\/3-540-63166-6_41"},{"key":"33_CR28","doi-asserted-by":"crossref","unstructured":"Kesten, Y., Pnueli, A.: Verification by augmented finitary abstraction. Information and Computation, Earlier version at MFCS, published in LNCS 1450 (2000) (to appear)","DOI":"10.1006\/inco.2000.3000"},{"key":"33_CR29","doi-asserted-by":"crossref","unstructured":"Lamport, L.: A new solution of Dijkstra\u2019s concurrent programming problem. C. ACM (August 1974)","DOI":"10.1145\/361082.361093"},{"key":"33_CR30","unstructured":"Lazi\u0107, R.S.: A Semantic Study of Data Independence with Applications to Model Checking. PhD thesis, Oxford University (1999)"},{"key":"33_CR31","doi-asserted-by":"crossref","unstructured":"Lee, D., Yannakakis, M.: Online minimization of transition systems. In: STOC (1992)","DOI":"10.1145\/129712.129738"},{"key":"33_CR32","unstructured":"Milner, R.: An algebraic definition of simulation between programs. In: 2nd IJCAI (1971)"},{"key":"33_CR33","doi-asserted-by":"crossref","unstructured":"Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol.\u00a0104. Springer, Heidelberg (1981)","DOI":"10.1007\/BFb0017309"},{"key":"33_CR34","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"33_CR35","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rodeh, Y., Shtrichman, O., Siegel, M.: Deciding equality formulas by small domains instantiations. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 455\u2013469. Springer, Heidelberg (1999)","DOI":"10.1007\/3-540-48683-6_39"},{"key":"33_CR36","doi-asserted-by":"crossref","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol.\u00a0137. Springer, Heidelberg (1982)","DOI":"10.1007\/3-540-11494-7_22"},{"key":"33_CR37","unstructured":"Sajid, K., Goel, A., Zhou, H., Aziz, A., Barber, S., Singhal, V.: Bdd- based procedures for a theory of equality with uninterpreted functions. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, Springer, Heidelberg (1998)"},{"key":"#cr-split#-33_CR38.1","doi-asserted-by":"crossref","unstructured":"Sipma, H., Uribe, T., Manna, Z.: Deductive model checking. CAV 1996??15 (1999);","DOI":"10.1023\/A:1008791913551"},{"key":"#cr-split#-33_CR38.2","unstructured":"Earlier version at Alur, R., Henzinger, T.A. (eds.): CAV 1996. LNCS, vol.??1102. Springer, Heidelberg (1996)"},{"key":"33_CR39","doi-asserted-by":"crossref","unstructured":"Wolper, P.: Expressing interesting properties of programs in propositional temporal logic. In: POPL (1986)","DOI":"10.1145\/512644.512661"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10722167_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,23]],"date-time":"2019-04-23T07:49:08Z","timestamp":1556005748000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10722167_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540677703","9783540450474"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/10722167_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}