{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,10]],"date-time":"2023-01-10T21:19:17Z","timestamp":1673385557904},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2002,12,18]],"date-time":"2002-12-18T00:00:00Z","timestamp":1040169600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2003,11]]},"DOI":"10.1007\/s10009-002-0088-z","type":"journal-article","created":{"date-parts":[[2004,3,20]],"date-time":"2004-03-20T15:40:18Z","timestamp":1079797218000},"page":"34-48","source":"Crossref","is-referenced-by-count":15,"title":["Finding feasible abstract counter-examples"],"prefix":"10.1007","volume":"5","author":[{"given":"Corina S.","family":"P\u0103s\u0103reanu","sequence":"first","affiliation":[]},{"given":"Matthew B.","family":"Dwyer","sequence":"additional","affiliation":[]},{"given":"Willem","family":"Visser","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,12,18]]},"reference":[{"key":"88_CR1","unstructured":"Abramsky, S., Hankin, C.: Abstract interpretation of declarative languages. Ellis Horwood, Chichester, UK, 1987"},{"key":"88_CR2","unstructured":"Arnold, K., Goslin, J.: The Java programming language. Addison-Wesley, Reading, Mass., USA, 1998"},{"key":"88_CR3","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M.B. (ed.), Model Checking Software, Proc. 8th International SPIN Workshop, Lecture Notes in Computer Science, vol. 2057. Springer, Berlin Heidelberg New York, 2001, pp. 103\u2013122","DOI":"10.1007\/3-540-45139-0_7"},{"key":"88_CR4","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Proc. 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI\u201901), ACM SIGPLAN Notices 36(5):203\u2013213, 2001","DOI":"10.1145\/381694.378846"},{"key":"88_CR5","doi-asserted-by":"crossref","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Boolean and Cartesian abstraction for model checking C programs. In: Margaria, T., Yi, W. (eds.), Proc. 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201901), Lecture Notes in Computer Science, vol. 2031. Springer, Berlin Heidelberg New York, 2001, pp. 268\u2013283","DOI":"10.1007\/3-540-45319-9_19"},{"key":"88_CR6","doi-asserted-by":"crossref","first-page":"410","DOI":"10.1007\/s100090050046","volume":"2","author":"Cimatti,","year":"4","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NuSMV: A new symbolic model checker. Int J Software Tools Technol Transfer 2(4):410\u2013425, 2000","journal-title":"Int J Software Tools Technol Transfer"},{"key":"88_CR7","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.), Proc. 12th International Conference on Computer-Aided Verification (CAV\u201900), Lecture Notes in Computer Science, vol. 1855. Springer, Berlin Heidelberg New York, 2000, pp. 154\u2013169","DOI":"10.1007\/10722167_15"},{"key":"88_CR8","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"Clarke,","year":"5","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans Program Lang Syst 16(5):1512\u20131542, 1994","journal-title":"ACM Trans Program Lang Syst"},{"key":"88_CR9","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Robby.: Expressing checkable properties of dynamic systems: the Bandera specification language. Int J Software Tools Technol Transfer (to appear)"},{"key":"88_CR10","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Robby.: Bandera: a source-level interface for model checking Java programs. In: Ghezzi, C., Jazayeri, M., Wolf, A. (eds.), Proc. 22nd International Conference on Software Engineering (ICSE\u201900), pp. 762\u2013765. ACM, New York, 2000"},{"key":"88_CR11","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., P\u0103s\u0103reanu, C.S., Robby, Zheng, H.: Bandera: extracting finite-state models from Java source code. In: Ghezzi, C., Jazayeri, M., Wolf, A. (eds.), Proc. of the 22nd International Conference on Software Engineering (ICSE\u201900), pp. 439\u2013448. ACM, 2000"},{"key":"88_CR12","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the 4th Annual ACM Symposium on Principles of Programming Languages, pp. 238\u2013252, 1977","DOI":"10.1145\/512950.512973"},{"key":"88_CR13","doi-asserted-by":"crossref","unstructured":"Dams, D., Gerth, R., D\u00f6hmen, G., Herrmann, R., Kelb, P., Pargmann, H.: Model checking using adaptive state and data abstraction. In: Dill, D.L. (ed.), Proc. 6th International Conference on Computer-Aided Verification (CAV\u201994), Lecture Notes in Computer Science, vol. 818. Springer, Berlin Heidelberg New York, 1994, pp. 455\u2013467","DOI":"10.1007\/3-540-58179-0_75"},{"key":"88_CR14","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1145\/244795.244800","volume":"19","author":"Dams,","year":"2","unstructured":"Dams, D., Gerth, R., Grumberg, O.: Abstract interpretation of reactive systems. ACM Trans Program Lang Syst 19(2):253\u2013291, 1997","journal-title":"ACM Trans Program Lang Syst"},{"key":"88_CR15","doi-asserted-by":"crossref","first-page":"577","DOI":"10.1002\/(SICI)1097-024X(199906)29:7<577::AID-SPE246>3.0.CO;2-V","volume":"29","author":"Demartini,","year":"7","unstructured":"Demartini, C., Iosif, R., Sisto, R.: A deadlock detection tool for concurrent Java programs. Software Pract Exper 29(7):577\u2013603, 1999","journal-title":"Software Pract Exper"},{"key":"88_CR16","unstructured":"Dwyer, M.B., Hatcliff, J., P\u0103s\u0103reanu, C.S., Robby.: Bandera case studies. Available at: http:\/\/www.cis.ksu.edu\/santos\/bandera\/#case-studies, 2001"},{"key":"88_CR17","unstructured":"Dwyer M.B., Wallentine, V.: Object-oriented coordination abstractions for parallel software. In: Proc. International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA\u201997), 1997"},{"key":"88_CR18","unstructured":"Dwyer, M.B., Hatcliff, J., Joehanes, R., Laubach, S., P\u0103s\u0103reanu, C.S., Robby, Visser, W., Zheng, H.: Tool-supported program abstraction for finite-state verification. In: Proc. 23rd International Conference on Software Engineering (ICSE\u201901), 2001"},{"key":"88_CR19","doi-asserted-by":"crossref","unstructured":"Giacobazzi, R., Quintarelli, E.: Incompleteness, counterexamples, and refinements in abstract model-checking. In: Cousot, P. (ed.), Proc. 8th International Static Analysis Symposium (SAS\u201901), Lecture Notes in Computer Science, vol. 2126. Springer, Berlin Heidelberg New York, 2001, pp. 356\u2013373","DOI":"10.1007\/3-540-47764-0_20"},{"key":"88_CR20","doi-asserted-by":"crossref","unstructured":"Hatcliff, J., Corbett, J.C., Dwyer, M.B., Sokolowski, S., Zheng, H.: A formal study of slicing for multi-threaded programs with JVM concurrency primitives. In: Cortesi, A., Fil\u00e9, G.(eds.), Proc. 6th International Static Analysis Symposium (SAS\u201999), Lecture Notes in Computer Science, vol. 1694. Springer, Berlin Heidelberg New York, 1999, pp. 1\u201318","DOI":"10.1007\/3-540-48294-6_1"},{"key":"88_CR21","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"Holzmann,","year":"5","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Transa Software Eng 23(5):279\u2013294, 1997","journal-title":"IEEE Transa Software Eng"},{"key":"88_CR22","doi-asserted-by":"crossref","unstructured":"Kesten, Y., Pnueli, A.: Modularization and abstraction: the keys to practical formal verification. In: Brim, L., Gruska, J., Zlatuska, J. (eds.), Proc. 23rd International Symposium on Mathematical Foundations of Computer Science (MFCS\u201998), Lecture Notes in Computer Science, vol. 1450. Springer, Berlin Heidelberg New York, 1998, pp. 54\u201371","DOI":"10.1007\/BFb0055757"},{"key":"88_CR23","doi-asserted-by":"crossref","unstructured":"Lakhnech, Y., Bensalem, S., Berezin, S., Owre, S.: Incremental verification by abstraction. In: Margaria, T., Yi, W. (eds.), Proc. 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201901), Lecture Notes in Computer Science, vol. 2301. Springer, Berlin Heidelberg New York, 2001, pp. 98\u2013112","DOI":"10.1007\/3-540-45319-9_8"},{"key":"88_CR24","unstructured":"Lea, D.: Concurrent programming in Java[tm], 2nd edn. Design principles and patterns. The Java Series. Addison-Wesley, Reading, Mass., USA, 1999"},{"key":"88_CR25","unstructured":"Lindholm, T., Yellin, F.: The Java virtual machine specification. Addison-Wesley, Reading, Mass., USA, 1999"},{"key":"88_CR26","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1007\/BF01384313","volume":"6","author":"Loiseaux,","year":"1","unstructured":"Loiseaux, C., Graf, S., Sifakis, J., Bouajiani, A., Bensalem, S.: Property preserving abstractions for the verification of concurrent systems. Formal Methods Syst Des 6(1):11\u201344, 1995","journal-title":"Formal Methods Syst Des"},{"key":"88_CR27","unstructured":"Magee, J., Kramer, J.: Concurrency: state models and Java programs. Wiley, New York, 1999"},{"key":"88_CR28","unstructured":"Penix, J., Visser, W., Engstrom, E., Larson, A., Weininger, N.: Verification of time partitioning in the DEOS real-time scheduling kernel. In: Ghezzi, C., Jazayeri, M., Wolf, A. (eds.), Proc. 22nd International Conference on Software Engineering (ICSE\u201900), pp. 488\u2013497. ACM, New York, 2000"},{"key":"88_CR29","doi-asserted-by":"crossref","unstructured":"P\u0103s\u0103reanu, C.S., Dwyer, M.B., Visser, W.: Finding feasible counter-examples when model checking abstracted Java programs. In: Margaria, T., Yi, W. (eds.), Proc. 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201901), Lecture Notes in Computer Science, vol. 2031. Springer, Berlin Heidelberg New York, 2001, pp. 284\u2013298","DOI":"10.1007\/3-540-45319-9_20"},{"key":"88_CR30","doi-asserted-by":"crossref","unstructured":"Rusu, V., Singerman, E.: On proving safety properties by integrating static analysis, theorem proving and abstraction. In: Cleaveland, R. (ed.), Proc. 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201999), Lecture Notes in Computer Science, vol. 1579. Springer, Berlin Heidelberg New York, 1999, pp. 178\u2013192","DOI":"10.1007\/3-540-49059-0_13"},{"key":"88_CR31","doi-asserted-by":"crossref","unstructured":"Sa\u00efdi, H.: Model checking guided abstraction and analysis. In: Palsberg, J. (ed.), Proc. 7th International Static Analysis Symposium (SAS\u201900), Lecture Notes in Computer Science, vol. 1824. Springer, Berlin Heidelberg New York, 2000, pp. 377\u2013396","DOI":"10.1007\/978-3-540-45099-3_20"},{"key":"88_CR32","unstructured":"Valle-Rai, R., Hendren, L., Sundaresan, V., Lam, P., Gagnon, E., Co, P.: Soot - a Java optimization framework. In: Proc. CASCON\u201999, 1999"},{"key":"88_CR33","doi-asserted-by":"crossref","unstructured":"Visser, W., Brat, G., Havelund, K., Park, S.: Model checking programs. In: Proc. 15th IEEE International Conference on Automated Software Engineering (ASE\u201900), pp. 3\u201312. IEEE Computer, New York, 2000","DOI":"10.1109\/ASE.2000.873645"},{"key":"88_CR34","doi-asserted-by":"crossref","unstructured":"Visser, W., Park, S., Penix, J.: Applying predicate abstraction to model check object-oriented programs. In: Proc. 3rd ACM SIGSOFT Workshop on Formal Methods in Software Practice, August 2000","DOI":"10.1145\/349360.351125"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-002-0088-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-002-0088-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-002-0088-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,31]],"date-time":"2020-03-31T18:11:18Z","timestamp":1585678278000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-002-0088-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,12,18]]},"references-count":34,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,11]]}},"alternative-id":["88"],"URL":"https:\/\/doi.org\/10.1007\/s10009-002-0088-z","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2002,12,18]]}}}