{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:04:45Z","timestamp":1725573885342},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540204619"},{"type":"electronic","value":"9783540398936"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-39893-6_33","type":"book-chapter","created":{"date-parts":[[2011,1,7]],"date-time":"2011-01-07T10:35:57Z","timestamp":1294396557000},"page":"579-598","source":"Crossref","is-referenced-by-count":4,"title":["Constraint-Based Model Checking of Data-Independent Systems"],"prefix":"10.1007","author":[{"given":"Beata","family":"Sarna-Starosta","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C. R.","family":"Ramakrishnan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"33_CR1","unstructured":"Aggarwal, S., Kurshan, R.P., Sabnani, K.: A calculus for protocol specification and validation. Protocol Specification, Testing and Verification, III (1983)"},{"key":"33_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/3-540-46002-0_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Basu","year":"2002","unstructured":"Basu, S., Narayan Kumar, K., Pokorny, L.R., Ramakrishnan, C.R.: Resourceconstrained model checking of recursive programs. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, p. 236. Springer, Heidelberg (2002)"},{"key":"33_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/3-540-45635-X_19","volume-title":"Logic Programming","author":"S. Basu","year":"2001","unstructured":"Basu, S., Mukund, M., Ramakrishnan, C.R., Ramakrishnan, I.V., Verma, R.M.: Local and symbolic bisimulation using tabled constraint logic programming. In: Codognet, P. (ed.) ICLP 2001. LNCS, vol.\u00a02237, p. 166. Springer, Heidelberg (2001)"},{"key":"33_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"T. Bultan","year":"1997","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)"},{"key":"33_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"W. Chan","year":"1997","unstructured":"Chan, W., Anderson, R.J., 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)"},{"key":"33_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-49059-0_16","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"G. Delzanno","year":"1999","unstructured":"Delzanno, G., Podelski, A.: Model checking in CLP. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, p. 223. Springer, Heidelberg (1999)"},{"key":"33_CR7","unstructured":"Du, X., Ramakrishnan, C.R., Smolka, S.A.: Tabled resolution + constraints: A recipe for model checking real-time systems. In: RTTS (2000)"},{"key":"33_CR8","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254. Springer, Heidelberg (1997)"},{"key":"33_CR9","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1016\/0304-3975(94)00172-F","volume":"138","author":"M. Hennessy","year":"1995","unstructured":"Hennessy, M., Lin, H.: Symbolic bisimulations. Theoretical Computer Science\u00a0138, 353\u2013389 (1995)","journal-title":"Theoretical Computer Science"},{"key":"33_CR10","doi-asserted-by":"crossref","unstructured":"Norris Ip, C., Dill, D.L.: Better verification through symmetry. FMSD (1996)","DOI":"10.1007\/BF00625968"},{"key":"33_CR11","doi-asserted-by":"crossref","unstructured":"Jaffar, J., Lassez, J.-L.: Constraint logic programming. In: POPL (1987)","DOI":"10.1145\/41625.41635"},{"key":"33_CR12","doi-asserted-by":"crossref","unstructured":"Jonsson, B., Parrow, J.: Deciding bisimulation equivalences for a class of nonfinite- state programs. Information and Computation\u00a0107(2) (December 1993)","DOI":"10.1006\/inco.1993.1069"},{"key":"33_CR13","unstructured":"Lazi\u0107, R.S.: A Semantic Study of Data Independence with Applications to Model Checking. PhD thesis, Oxford University (1999)"},{"key":"33_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0014474","volume-title":"CONCUR \u201996: Concurrency Theory","author":"H. Lin","year":"1996","unstructured":"Lin, H.: Symbolic transition graphs with assignments. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol.\u00a01119. Springer, Heidelberg (1996)"},{"key":"33_CR15","unstructured":"Lin, H.: Model checking value-passing processes. In: APSEC (2001)"},{"key":"33_CR16","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-96826-6","volume-title":"Foundations of Logic Programming","author":"J.W. Lloyd","year":"1984","unstructured":"Lloyd, J.W.: Foundations of Logic Programming. Springer, Heidelberg (1984)"},{"key":"33_CR17","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems","author":"Z. Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, Heidelberg (1992)"},{"key":"33_CR18","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"K.S. Namjoshi","year":"2000","unstructured":"Namjoshi, K.S., Kurshan, R.P.: Syntactic program transformations for automatic abstractions. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855. Springer, Heidelberg (2000)"},{"key":"33_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/3-540-45619-8_8","volume-title":"Logic Programming","author":"G. Pemmasani","year":"2002","unstructured":"Pemmasani, G., Ramakrishnan, C.R., Ramakrishnan, I.V.: Efficient model checking of real time systems using tabled logic programming and constraints. In: Stuckey, P.J. (ed.) ICLP 2002. LNCS, vol.\u00a02401, p. 100. Springer, Heidelberg (2002)"},{"key":"33_CR20","unstructured":"Pnueli, A., Kesten, Y., Vardi, M.: Yes, Matilda! Abstraction can Replace Deduction, even for Computational Models which are BAD (Buchi Automata with Data). In: VHS Meeting, Grenoble (1999)"},{"key":"33_CR21","doi-asserted-by":"crossref","unstructured":"Robert Pokorny, L., Ramakrishnan, C.R.: Model checking linear temporal logic using tabled logic programming. In: TAPD (2000)","DOI":"10.1007\/3-540-44618-4_8"},{"issue":"1 \/ 2","key":"33_CR22","doi-asserted-by":"crossref","first-page":"189","DOI":"10.3233\/JCS-2002-101-209","volume":"10","author":"C.R. Ramakrishnan","year":"2002","unstructured":"Ramakrishnan, C.R., Sekar, R.: Model-based analysis of configuration vulnerabilities. Journal of Computer Security (JCS)\u00a010(1 \/ 2), 189\u2013209 (2002)","journal-title":"Journal of Computer Security (JCS)"},{"key":"33_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_48","volume-title":"Computer Aided Verification","author":"C.R. Ramakrishnan","year":"2000","unstructured":"Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A., et al.: XMC: A logicprogramming- based verification toolset. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855. Springer, Heidelberg (2000)"},{"key":"33_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/3-540-44585-4_13","volume-title":"Computer Aided Verification","author":"Y. Rodeh","year":"2001","unstructured":"Rodeh, Y., Shtrichman, O.: Finite instantiations in equivalence logic with uninterpreted functions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, p. 144. Springer, Heidelberg (2001)"},{"key":"33_CR25","doi-asserted-by":"crossref","unstructured":"Roychoudhury, A., Ramakrishnan, C.R., Ramakrishnan, I.V.: Justifying proofs using memo tables. In: PPDP (2000)","DOI":"10.1145\/351268.351290"},{"key":"33_CR26","series-title":"Lecture Notes in Computer Science","volume-title":"Third International Conference on Logic Programming","author":"H. Tamaki","year":"1986","unstructured":"Tamaki, H., Sato, T.: OLDT resolution with tabulation. In: Shapiro, E. (ed.) ICLP 1986. LNCS, vol.\u00a0225. Springer, Heidelberg (1986)"},{"key":"33_CR27","doi-asserted-by":"crossref","unstructured":"Wolper, P.: Expressing interesting properties of programs in propositional temporal logic. In: POPL (1986)","DOI":"10.1145\/512644.512661"},{"key":"33_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/3-540-36384-X_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P. Yang","year":"2002","unstructured":"Yang, P., Ramakrishnan, C.R., Smolka, S.A.: A logical encoding of the picalculus: Model checking mobile processes using tabled resolution. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol.\u00a02575, pp. 116\u2013131. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-39893-6_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T13:43:22Z","timestamp":1559915002000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39893-6_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540204619","9783540398936"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39893-6_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}