{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:33:33Z","timestamp":1773192813254,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540474609","type":"print"},{"value":"9783540474623","type":"electronic"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11901433_30","type":"book-chapter","created":{"date-parts":[[2006,11,20]],"date-time":"2006-11-20T12:40:51Z","timestamp":1164026451000},"page":"549-567","source":"Crossref","is-referenced-by-count":8,"title":["Optimized Execution of Deterministic Blocks in Java PathFinder"],"prefix":"10.1007","author":[{"given":"Marcelo","family":"d\u2019Amorim","sequence":"first","affiliation":[]},{"given":"Ahmed","family":"Sobeih","sequence":"additional","affiliation":[]},{"given":"Darko","family":"Marinov","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"30_CR1","unstructured":"J-Sim, http:\/\/www.j-sim.org\/"},{"key":"30_CR2","unstructured":"Java Native Interface: Programmer\u2019s Guide and Specification. Online book, http:\/\/java.sun.com\/docs\/books\/jni\/"},{"key":"30_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/3-540-45139-0_7","volume-title":"Model Checking Software","author":"T. Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 103\u2013122. Springer, Heidelberg (2001)"},{"issue":"4","key":"30_CR4","doi-asserted-by":"publisher","first-page":"538","DOI":"10.1145\/581771.581775","volume":"49","author":"K. Bhargavan","year":"2002","unstructured":"Bhargavan, K., Obradovic, D., Gunter, C.A.: Formal verification of standards for distance vector routing protocols. Journal of the ACM\u00a049(4), 538\u2013576 (2002)","journal-title":"Journal of the ACM"},{"key":"30_CR5","doi-asserted-by":"crossref","unstructured":"Boyapati, C., Khurshid, S., Marinov, D.: Korat: automated testing based on Java predicates. In: Proc. International Symposium on Software Testing and Analysis, pp. 123\u2013133 (2002)","DOI":"10.1145\/566171.566191"},{"key":"30_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"key":"30_CR7","doi-asserted-by":"crossref","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Pasareanu, C.S., Robby, Zheng, H.: Bandera: extracting finite-state models from Java source code. In: Proc. 22nd International Conference on Software Engineering, pp. 439\u2013448 (2000)","DOI":"10.1145\/337180.337234"},{"key":"30_CR8","doi-asserted-by":"publisher","first-page":"1025","DOI":"10.1002\/spe.602","volume":"34","author":"C. Csallner","year":"2004","unstructured":"Csallner, C., Smaragdakis, Y.: JCrasher: an automatic robustness tester for Java. Software: Practice and Experience\u00a034, 1025\u20131050 (2004)","journal-title":"Software: Practice and Experience"},{"key":"30_CR9","doi-asserted-by":"crossref","unstructured":"Dill, D.L., Drexler, A.J., Hu, A.J., Yang, C.H.: Protocol verification as a hardware design aid. In: IEEE International Conference on Computer Design (IEEE ICCD), pp. 522\u2013525 (1992)","DOI":"10.1109\/ICCD.1992.276232"},{"key":"30_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1007\/978-3-540-27813-9_46","volume-title":"Computer Aided Verification","author":"A. Farzan","year":"2004","unstructured":"Farzan, A., Chen, F., Meseguer, J., Rosu, G.: Formal analysis of Java programs in JavaFAN. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 501\u2013505. Springer, Heidelberg (2004)"},{"key":"30_CR11","volume-title":"Java In A Nutshell","author":"D. Flanagan","year":"1997","unstructured":"Flanagan, D.: Java In A Nutshell. O\u2019Reilly, Sebastopol (1997)"},{"key":"30_CR12","unstructured":"Foundations of Software Engineering at Microsoft Research. The AsmL test generator tool, http:\/\/research.microsoft.com\/fse\/asml\/doc\/AsmLTester.html"},{"key":"30_CR13","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Model checking for programming languages using Verisoft. In: Proc. 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 174\u2013186 (1997)","DOI":"10.1145\/263699.263717"},{"key":"30_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/3-540-48234-2_11","volume-title":"Theoretical and Practical Aspects of SPIN Model Checking","author":"K. Havelund","year":"1999","unstructured":"Havelund, K.: Java Pathfinder, a translator from Java to Promela. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol.\u00a01680, p. 152. Springer, Heidelberg (1999)"},{"issue":"5","key":"30_CR15","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. on Software Engineering\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. on Software Engineering"},{"key":"30_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/3-540-46017-9_5","volume-title":"Model Checking Software","author":"R. Iosif","year":"2002","unstructured":"Iosif, R.: Symmetry reduction criteria for software model checking. In: Bo\u0161na\u010dki, D., Leue, S. (eds.) SPIN 2002. LNCS, vol.\u00a02318, pp. 22\u201341. Springer, Heidelberg (2002)"},{"key":"30_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/3-540-45139-0_6","volume-title":"Model Checking Software","author":"F. Lerda","year":"2001","unstructured":"Lerda, F., Visser, W.: Addressing dynamic issues of program model checking. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 80\u2013102. Springer, Heidelberg (2001)"},{"key":"30_CR18","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)"},{"key":"30_CR19","unstructured":"Mehlitz, P.C., Visser, W., Penix, J.: The JPF runtime verification system. Online manual, http:\/\/javapathfinder.sourceforge.net\/JPF.pdf"},{"key":"30_CR20","series-title":"Lecture Notes in Computer Science","first-page":"28","volume-title":"Model Checking Software","author":"M. Musuvathi","year":"2007","unstructured":"Musuvathi, M., Dill, D.L.: An incremental heap canonicalization algorithm. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol.\u00a04595, pp. 28\u201342. Springer, Heidelberg (2007)"},{"key":"30_CR21","unstructured":"Musuvathi, M., Engler, D.: Model checking large network protocol implementations. In: Proc. of The First Symposium on Networked Systems Design and Implementation (NSDI), pp. 155\u2013168 (2004)"},{"key":"30_CR22","doi-asserted-by":"crossref","unstructured":"Musuvathi, M., Park, D., Chou, A., Engler, D.R., Dill, D.L.: CMC: A pragmatic approach to model checking real code. In: Proc. 5th Symposium on Operating Systems Design and Implementation, pp. 75\u201388 (December 2002)","DOI":"10.1145\/1060289.1060297"},{"key":"30_CR23","doi-asserted-by":"crossref","unstructured":"Pacheco, C., Ernst, M.D.: Eclat: Automatic generation and classification of test inputs. In: Proc. 19th European Conference on Object-Oriented Programming, Glasgow, Scotland, pp. 504\u2013527 (July 2005)","DOI":"10.1007\/11531142_22"},{"key":"30_CR24","doi-asserted-by":"crossref","unstructured":"Park, D.Y., Stern, U., Skakkeb\u00e6k, J.U., Dill, D.L.: Java model checking. In: Proc. of IEEE ASE 2000 (2000)","DOI":"10.1109\/ASE.2000.873671"},{"key":"30_CR25","doi-asserted-by":"crossref","unstructured":"Perkins, C.E., Belding-Royer, E.M., Das, S.: Ad hoc on demand distance vector (aodv) routing. IETF Draft (January 2002)","DOI":"10.17487\/rfc3561"},{"key":"30_CR26","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1109\/MCSA.1999.749281","volume-title":"Proc. IEEE Workshop on Mobile Computing Systems and Applications (WMCSA)","author":"C.E. Perkins","year":"1999","unstructured":"Perkins, C.E., Royer, E.M.: Ad-hoc on-demand distance vector routing. In: Proc. IEEE Workshop on Mobile Computing Systems and Applications (WMCSA), pp. 90\u2013100. IEEE Computer Society Press, Los Alamitos (1999)"},{"key":"30_CR27","doi-asserted-by":"crossref","unstructured":"Robby, Dwyer, M.B., Hatcliff, J.: Bogor: an extensible and highly-modular software model checking framework. In: Proc. 9th European Software Engineering Conference held jointly with 11th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 267\u2013276 (2003)","DOI":"10.1145\/940103.940107"},{"key":"30_CR28","unstructured":"Sobeih, A., Viswanathan, M., Hou, J.C.: Incorporating bounded model checking in network simulation: Theory, implementation and evaluation. Technical Report UIUCDCS-R-2004-2466, Department of Computer Science, University of Illinois at Urbana-Champaign, Urbana, Illinois (July 2004)"},{"key":"30_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/11576280_17","volume-title":"Formal Methods and Software Engineering","author":"A. Sobeih","year":"2005","unstructured":"Sobeih, A., Viswanathan, M., Marinov, D., Hou, J.C.: Finding bugs in network protocols using simulation code and protocol-specific heuristics. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol.\u00a03785, pp. 235\u2013250. Springer, Heidelberg (2005)"},{"key":"30_CR30","doi-asserted-by":"crossref","unstructured":"Stotts, D., Lindsey, M., Antley, A.: An informal formal method for systematic JUnit test case generation. In: Proc. 2002 XP\/Agile Universe, pp. 131\u2013143 (2002)","DOI":"10.1007\/3-540-45672-4_13"},{"key":"30_CR31","unstructured":"Tyan, H.-Y.: Design, Realization and Evaluation of a Component-based Compositional Software Architecture for Network Simulation. Ph.D., Department of Electrical Engineering, The Ohio State University (2002)"},{"key":"30_CR32","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1145\/1081706.1081751","volume-title":"ESEC\/FSE-13: Proc. of the 10th European Software Engineering Conference and the 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering","author":"M. Veanes","year":"2005","unstructured":"Veanes, M., Campbell, C., Schulte, W., Tillmann, N.: Online testing with model programs. In: ESEC\/FSE-13: Proc. of the 10th European Software Engineering Conference and the 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 273\u2013282. ACM Press, New York (2005)"},{"key":"30_CR33","doi-asserted-by":"crossref","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S.: Model checking programs. In: Proc. 15th IEEE International Conference on Automated Software Engineering (2000)","DOI":"10.1109\/ASE.2000.873645"},{"key":"30_CR34","doi-asserted-by":"crossref","unstructured":"Visser, W., Pasareanu, C.S., Khurshid, S.: Test input generation with Java PathFinder. In: Proc. 2004 ACM SIGSOFT International Symposium on Software Testing and Analysis, pp. 97\u2013107 (2004)","DOI":"10.1145\/1007512.1007526"},{"key":"30_CR35","doi-asserted-by":"crossref","unstructured":"Visser, W., Pasareanu, C.S., Pelanek, R.: Test input generation for red-black trees using abstraction. In: Proc. of IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 414\u2013417 (2005)","DOI":"10.1145\/1101908.1101983"},{"key":"30_CR36","doi-asserted-by":"crossref","unstructured":"Visser, W., Pasareanu, C.S., Pelanek, R.: Test input generation for Java containers using state matching. In: Proc. 2006 ACM SIGSOFT International Symposium on Software Testing and Analysis (2006)","DOI":"10.1145\/1146238.1146243"},{"key":"30_CR37","unstructured":"Xie, T., Marinov, D., Notkin, D.: Rostra: A framework for detecting redundant object-oriented unit tests. In: Proc. 19th ASE, pp. 196\u2013205 (September 2004)"},{"key":"30_CR38","doi-asserted-by":"crossref","unstructured":"Xie, T., Marinov, D., Schulte, W., Notkin, D.: Symstra: A framework for generating object-oriented unit tests using symbolic execution. In: Proc. 11th TACAS, pp. 365\u2013381 (April 2005)","DOI":"10.1007\/978-3-540-31980-1_24"},{"key":"30_CR39","unstructured":"Yang, J., Twohey, P., Engler, D.R., Musuvathi, M.: Using model checking to find serious file system errors. In: OSDI, pp. 273\u2013288 (2004)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11901433_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,12]],"date-time":"2025-01-12T00:26:14Z","timestamp":1736641574000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11901433_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540474609","9783540474623"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/11901433_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}