{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:59:00Z","timestamp":1725551940121},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540311393"},{"type":"electronic","value":"9783540316220"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11609773_2","type":"book-chapter","created":{"date-parts":[[2005,12,12]],"date-time":"2005-12-12T07:28:57Z","timestamp":1134372537000},"page":"17-32","source":"Crossref","is-referenced-by-count":5,"title":["A CLP Method for Compositional and Intermittent Predicate Abstraction"],"prefix":"10.1007","author":[{"given":"Joxan","family":"Jaffar","sequence":"first","affiliation":[]},{"given":"Andrew E.","family":"Santosa","sequence":"additional","affiliation":[]},{"given":"R\u0103zvan","family":"Voicu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: 15th PLDI, May 2001. SIGPLAN Notices, vol.\u00a036(5), pp. 203\u2013213 (2001)","DOI":"10.1145\/381694.378846"},{"issue":"2","key":"2_CR2","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1145\/1057387.1057391","volume":"27","author":"T. Ball","year":"2005","unstructured":"Ball, T., Millstein, T., Rajamani, S.K.: Polymorphic predicate abstraction. ACM Transactions on Programming Languages and Systems\u00a027(2), 314\u2013343 (2005)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"2_CR3","unstructured":"Barras, B., Boutin, S., Cornes, C., Courant, J., Filliatre, J., Gim\u00e9nez, E., Herbelin, H., Huet, G., Noz, C.M., Murthy, C., Parent, C., Paulin, C., Sa\u00efbi, A., Werner, B.: The Coq proof assistant reference manual\u2014version v6.1. Technical Report 0203, INRIA (1997)"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"Logic-Based Program Synthesis and Transformation","year":"2000","unstructured":"Bossi, A. (ed.): LOPSTR 1999. LNCS, vol.\u00a01817. Springer, Heidelberg (2000)"},{"issue":"6","key":"2_CR5","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1109\/TSE.2004.22","volume":"30","author":"S. Chaki","year":"2004","unstructured":"Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. IEEE Transactions on Software Engineering\u00a030(6), 388\u2013402 (2004)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-30569-9_6","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"D.R. Cok","year":"2005","unstructured":"Cok, D.R., Kiniry, J.: ESC\/Java2: Uniting ESC\/Java and JML. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 108\u2013128. Springer, Heidelberg (2005)"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55844-6_142","volume-title":"Programming Language Implementation and Logic Programming","author":"P. Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Comparing the Galois connection and widening\/narrowing approaches to abstract interpretation. In: Bruynooghe, M., Wirsing, M. (eds.) PLILP 1992. LNCS, vol.\u00a0631. Springer, Heidelberg (1992)"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-48683-6_16","volume-title":"Computer Aided Verification","author":"S. Das","year":"1999","unstructured":"Das, S., Dill, D.L., Park, S.: Experience with predicate abstraction. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 160\u2013171. Springer, Heidelberg (1999)"},{"key":"2_CR9","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, pp. 223\u2013239. Springer, Heidelberg (1999)"},{"key":"2_CR10","volume-title":"21st RTSS","author":"X. Du","year":"2000","unstructured":"Du, X., Ramakrishnan, C.R., Smolka, S.A.: Tabled resolution + constraints: A recipe for model checking real-time systems. In: 21st RTSS. IEEE Computer Society Press, Los Alamitos (2000)"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"FME 2003: Formal Methods","author":"L. Burdy","year":"2003","unstructured":"Burdy, L., et al.: Java applet correctness: A developer-oriented approach. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805. Springer, Heidelberg (2003)"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Ramakrishna, Y.S., et al.: Efficient model checking using tabled resolution. In: Grumberg [16]","DOI":"10.1007\/3-540-63166-6_16"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Fioravanti, F., Pettorossi, A., Proietti, M.: Verifying CTL properties of infinite-state systems by specializing constraint logic programs. In: Leuschel, M., Podelski, A., Ramakrishnan, C.R., Ultes-Nitsche, U. (eds.) 2nd VCL, pp. 85\u201396 (2001)","DOI":"10.1007\/3-540-45142-0_8"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Fribourg, L.: Constraint logic programming applied to model checking. In: Bossi [4], pp. 30\u201341","DOI":"10.1007\/10720327_3"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs of infinite systems with PVS. In: Grumberg [16], pp. 72\u201383","DOI":"10.1007\/3-540-63166-6_10"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","year":"1997","unstructured":"Grumberg, O. (ed.): CAV 1997. LNCS, vol.\u00a01254. Springer, Heidelberg (1997)"},{"key":"2_CR17","first-page":"230","volume-title":"18th RTSS","author":"G. Gupta","year":"1997","unstructured":"Gupta, G., Pontelli, E.: A constraint-based approach for specification and verification of real-time systems. In: 18th RTSS, pp. 230\u2013239. IEEE Computer Society Press, Los Alamitos (1997)"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BFb0031814","volume-title":"Formal Methods in Computer-Aided Design","author":"J. Harrison","year":"1996","unstructured":"Harrison, J.: HOL light: A tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 265\u2013269. Springer, Heidelberg (1996)"},{"key":"2_CR19","series-title":"SIGPLAN Notices","first-page":"58","volume-title":"29th POPL","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R.: Lazy abstraction. In: 29th POPL. SIGPLAN Notices, vol.\u00a037(1), pp. 58\u201370. ACM Press, New York (2002)"},{"key":"2_CR20","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Add.-Wesley, Reading (2003)"},{"key":"2_CR21","first-page":"449","volume-title":"New Generation Computing","author":"J. Jaffar","year":"1993","unstructured":"Jaffar, J., Maher, M., Stuckey, P., Yap, R.: Projecting CLP( $\\cal R$ ) constraints. In: New Generation Computing, vol.\u00a011, pp. 449\u2013469. Ohmsha and Springer, Heidelberg (1993)"},{"issue":"3","key":"2_CR22","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1145\/129393.129398","volume":"14","author":"J. Jaffar","year":"1992","unstructured":"Jaffar, J., Michaylov, S., Stuckey, P.J., Yap, R.H.C.: The CLP( $\\cal R$ ) language and system. ACM TOPLAS\u00a014(3), 339\u2013395 (1992)","journal-title":"ACM TOPLAS"},{"key":"2_CR23","unstructured":"Leuschel, M., Massart, T.: Infinite-state model checking by abstract interpretation and program specialization. In: Bossi [4]"},{"issue":"1\u20132","key":"2_CR24","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/j.jlap.2003.07.006","volume":"58","author":"C. March\u00e9","year":"2004","unstructured":"March\u00e9, C., Paulin-Mohring, C., Urbain, X.: The KRAKATOA tool for certification of JAVA\/JAVACARD programs annotated in JML. J. Log. and Alg. Prog.\u00a058(1\u20132), 89\u2013106 (2004)","journal-title":"J. Log. and Alg. Prog."},{"key":"2_CR25","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-03811-6","volume-title":"Principles of Program Analysis","author":"F. Nielson","year":"1999","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999)"},{"key":"2_CR26","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1007\/3-540-44957-4_26","volume-title":"Computational Logic - CL 2000","author":"U. Nilsson","year":"2000","unstructured":"Nilsson, U., L\u00fcbcke, J.: Constraint logic programming for local and symbolic model checking. In: Palamidessi, C., Moniz Pereira, L., Lloyd, J.W., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. LNCS (LNAI), vol.\u00a01861, pp. 384\u2013398. Springer, Heidelberg (2000)"},{"key":"2_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Shankar, N., Rushby, J.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"}],"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\/11609773_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,5]],"date-time":"2023-05-05T21:28:37Z","timestamp":1683322117000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11609773_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540311393","9783540316220"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/11609773_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}