{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:34:05Z","timestamp":1773192845838,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540213147","type":"print"},{"value":"9783540247326","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24732-6_13","type":"book-chapter","created":{"date-parts":[[2010,7,28]],"date-time":"2010-07-28T00:14:47Z","timestamp":1280276087000},"page":"164-181","source":"Crossref","is-referenced-by-count":51,"title":["Verification of Java Programs Using Symbolic Execution and Invariant Generation"],"prefix":"10.1007","author":[{"given":"Corina S.","family":"P\u0103s\u0103reanu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Willem","family":"Visser","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.: Automatic predicate abstraction of C programs. In: Proc. PLDI, pp. 203\u2013213 (2001)","DOI":"10.1145\/378795.378846"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/3-540-46002-0_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Ball","year":"2002","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Relative completeness of abstraction refinement for software model checking. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, p. 158. Springer, Heidelberg (2002)"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"S. Bensalem","year":"1996","unstructured":"Bensalem, S., Lakhnech, Y., Saidi, H.: Powerful techniques for the automatic generation of invariants. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, Springer, Heidelberg (1996)"},{"key":"13_CR4","first-page":"227","volume":"16","author":"N. Bjorner","year":"2000","unstructured":"Bjorner, N., Browne, A., Colon, M., Finkbeiner, B., Manna, Z., Sipma, H., Uribe, T.: Verifying temporal properties of reactive systems: A STeP tutorial. FMSD\u00a016, 227\u2013270 (2000)","journal-title":"FMSD"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-540-45069-6_39","volume-title":"Computer Aided Verification","author":"M. Colon","year":"2003","unstructured":"Colon, M., Sankaranarayanan, S., Sipma, H.: Linear invariant generation using non-linear constraint solving. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 420\u2013432. Springer, Heidelberg (2003)"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Corbett, J., Dwyer, M., Hatcliff, J., Laubach, S., P\u0103s\u0103reanu, C., Robby, Zheng, H.: Bandera : Extracting finite-state models from Java source code. In: Proc. ICSE 2000 (2000)","DOI":"10.1145\/337180.337234"},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/3-540-45657-0_3","volume-title":"Computer Aided Verification","author":"P. Cousot","year":"2002","unstructured":"Cousot, P., Cousot, R.: On abstraction in software verification. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 37. Springer, Heidelberg (2002)"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proc. 5th POPL (1978)","DOI":"10.1145\/512760.512770"},{"key":"13_CR9","unstructured":"Delzanno, G., Podelski, A.: Widen, narrow and relax. Technical report"},{"key":"13_CR10","unstructured":"Detlefs, D.L., Leino, K.R.M., Nelson, G., Saxe, J.B.: Extended static checking. Research Report 159, Compaq Systems Research Center (1998)"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-3-540-45099-3_7","volume-title":"Static Analysis","author":"N. Dor","year":"2000","unstructured":"Dor, N., Rodeh, M., Sagiv, M.: Checking cleanness in linked lists. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol.\u00a01824, pp. 115\u2013135. Springer, Heidelberg (2000)"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Ernst, M.D., Czeisler, A., Griswold, W.G., Notkin, D.: Quickly detecting relevant program invariants. In: Proc. ICSE. ACM (2000)","DOI":"10.1109\/ICSE.2000.870435"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: Proc. POPL (2002)","DOI":"10.1145\/503272.503291"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Proc. Symposia in Applied Mathematics, vol.\u00a019, pp. 19\u201332 (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Model checking for programming languages using VeriSoft. In: Proc. POPL, pp. 174\u2013186, Paris, France (January 1997)","DOI":"10.1145\/263699.263717"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"196","DOI":"10.1007\/3-540-61474-5_69","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1996","unstructured":"Graf, S., Saidi, H.: Verifying invariants using theorem proving. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 196\u2013207. Springer, Heidelberg (1996)"},{"key":"13_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","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, pp. 72\u201383. Springer, Heidelberg (1997)"},{"issue":"3","key":"13_CR18","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1145\/356674.356677","volume":"8","author":"S.L. Hantler","year":"1976","unstructured":"Hantler, S.L., King, J.C.: An introduction to proving the correctness of programs. ACM Comput. Surv.\u00a08(3), 331\u2013353 (1976)","journal-title":"ACM Comput. Surv."},{"key":"13_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"662","DOI":"10.1007\/3-540-60973-3_113","volume-title":"FME \u201996: Industrial Benefit and Advances in Formal Methods","author":"K. Havelund","year":"1996","unstructured":"Havelund, K., Shankar, N.: Experiments in theorem proving and model checking for protocol verification. In: Gaudel, M.-C., Woodcock, J.C.P. (eds.) FME 1996. LNCS, vol.\u00a01051, pp. 662\u2013681. Springer, Heidelberg (1996)"},{"issue":"10","key":"13_CR20","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM\u00a012(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"13_CR21","unstructured":"Holzmann, G.: The Spin Model Checker: Primer and Reference Manual (2003)"},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"Karr, M.: Affine relationships among variables of a program. Acta Informatica\u00a06 (1976)","DOI":"10.1007\/BF00268497"},{"key":"13_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"553","DOI":"10.1007\/3-540-36577-X_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Khurshid","year":"2003","unstructured":"Khurshid, S., P\u0103s\u0103reanu, C.S., Visser, W.: Generalized symbolic execution for model checking and testing. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 553\u2013568. Springer, Heidelberg (2003)"},{"issue":"7","key":"13_CR24","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"J.C. King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM\u00a019(7), 385\u2013394 (1976)","journal-title":"Commun. ACM"},{"key":"13_CR25","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification (1992)","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"13_CR26","doi-asserted-by":"crossref","unstructured":"Moeller, A., Schwartzbach, M.I.: The pointer assertion logic engine. In: Proc. PLDI, Snowbird, UT (June 2001)","DOI":"10.1145\/378795.378851"},{"key":"13_CR27","doi-asserted-by":"crossref","unstructured":"Pugh, W.: The Omega test: A fast and practical integer programming algorithm for dependence analysis. Communications of the ACM\u00a031(8) (August 1992)","DOI":"10.1145\/135226.135233"},{"key":"13_CR28","doi-asserted-by":"crossref","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Solving shape-analysis problems in languages with destructive updating. ACM Trans. Prog. Lang. Syst. (January 1998)","DOI":"10.1145\/271510.271517"},{"key":"13_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/3-540-45319-9_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Tiwari","year":"2001","unstructured":"Tiwari, A., Rues, H., Saidi, H., Shankar, N.: A technique for invariant generation. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, p. 113. Springer, Heidelberg (2001)"},{"key":"13_CR30","doi-asserted-by":"crossref","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S.: Model checking programs. In: Proc. ASE, Grenoble, France (2000)","DOI":"10.1109\/ASE.2000.873645"},{"issue":"2","key":"13_CR31","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1145\/360827.360850","volume":"17","author":"B. Wegbreit","year":"1974","unstructured":"Wegbreit, B.: The synthesis of loop predicates. Communications of the ACM\u00a017(2), 102\u2013112 (1974)","journal-title":"Communications of the ACM"},{"key":"13_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/BFb0028736","volume-title":"Computer Aided Verification","author":"P. Wolper","year":"1998","unstructured":"Wolper, P., Boigelot, B.: Verifying systems with infinite but regular state spaces. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 88\u201397. Springer, Heidelberg (1998)"},{"key":"13_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/3-540-45789-5_8","volume-title":"Static Analysis","author":"T. Yavuz-Kahveci","year":"2002","unstructured":"Yavuz-Kahveci, T., Bultan, T.: Automated verification of concurrent linked lists with counters. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol.\u00a02477, p. 69. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24732-6_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T19:30:15Z","timestamp":1559331015000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24732-6_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540213147","9783540247326"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24732-6_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}