{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:55:43Z","timestamp":1725551743455},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540297970"},{"type":"electronic","value":"9783540322504"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11576280_17","type":"book-chapter","created":{"date-parts":[[2005,10,24]],"date-time":"2005-10-24T10:01:26Z","timestamp":1130148086000},"page":"235-250","source":"Crossref","is-referenced-by-count":8,"title":["Finding Bugs in Network Protocols Using Simulation Code and Protocol-Specific Heuristics"],"prefix":"10.1007","author":[{"given":"Ahmed","family":"Sobeih","sequence":"first","affiliation":[]},{"given":"Mahesh","family":"Viswanathan","sequence":"additional","affiliation":[]},{"given":"Darko","family":"Marinov","sequence":"additional","affiliation":[]},{"given":"Jennifer C.","family":"Hou","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","unstructured":"Saha, A.K., To, K., PalChaudhuri, S., Du, S., Johnson, D.B.: Physical implementation of ad hoc network routing protocols using unmodified ns-2 models. In: ACM MobiCom 2004, Poster (2004)"},{"key":"17_CR2","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)"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Musuvathi, M., Park, D.Y.W., Chou, A., Engler, D.R., Dill, D.L.: CMC: A pragmatic approach to model checking real code. In: Proc. of OSDI 2002 (2002)","DOI":"10.1145\/1060289.1060297"},{"key":"17_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/3-540-44585-4_25","volume-title":"Computer Aided Verification","author":"T. Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.K.: The SLAM Toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, p. 260. Springer, Heidelberg (2001)"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular Verification of Software Components in C. In: Proc. of ICSE 2003 (2003)","DOI":"10.1109\/ICSE.2003.1201217"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy Abstraction. In: Proc. of POPL 2002 (2002)","DOI":"10.1145\/503272.503279"},{"key":"17_CR7","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":"17_CR8","unstructured":"J-Sim, http:\/\/www.j-sim.org\/"},{"key":"17_CR9","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Sobeih, A., Viswanathan, M., Hou, J.C.: Check and Simulate: A case for incorporating model checking in network simulation. In: Proc. of ACM-IEEE MEMOCODE 2004 (2004)","DOI":"10.1109\/MEMCOD.2004.1459810"},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"Perkins, C.E., Royer, E.M.: Ad-hoc on-demand distance vector routing. In: Proc. of IEEE WMCSA 1999 (1999)","DOI":"10.1109\/MCSA.1999.749281"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Perkins, C.E., Royer, E.M., Das, S.: Ad hoc on demand distance vector (aodv) routing, IETF Draft (January 2002)","DOI":"10.17487\/rfc3561"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"Intanagonwiwat, C., Govindan, R., Estrin, D.: Directed diffusion: A scalable and robust communication paradigm for sensor networks. In: Proc. of ACM MobiCom 2000 (2000)","DOI":"10.1145\/345910.345920"},{"key":"17_CR14","unstructured":"Musuvathi, M., Engler, D.R.: Model checking large network protocol implementations. In: Proc. of NSDI 2004 (2004)"},{"issue":"2-3","key":"17_CR15","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/s10009-002-0104-3","volume":"5","author":"S. Edelkamp","year":"2004","unstructured":"Edelkamp, S., Leue, S., Lluch-Lafuente, A.: Directed Explicit-State Model Checking in the Validation of Communication Protocols. International Journal on Software Tools for Technology Transfer (STTT)\u00a05(2-3), 247\u2013267 (2004)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"key":"17_CR16","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1109\/TSSC.1968.300136","volume":"4","author":"P.E. Hart","year":"1968","unstructured":"Hart, P.E., Nilsson, N.J., Raphael, B.: A formal basis for heuristic determination of minimum path cost. IEEE Transactions on Systems Science and Cybernetics\u00a04, 100\u2013107 (1968)","journal-title":"IEEE Transactions on Systems Science and Cybernetics"},{"key":"17_CR17","unstructured":"Sobeih, A., Viswanathan, M., Hou, J.C.: Incorporating Bounded Model Checking in Network Simulation: Theory, Implementation and Evaluation, Tech. Rep. UIUCDCS-R-2004-2466, Department of Computer Science, University of Illinois at Urbana-Champaign (July 2004)"},{"issue":"4","key":"17_CR18","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":"17_CR19","doi-asserted-by":"crossref","unstructured":"Sobeih, A., Viswanathan, M., Hou, J.C.: Bounded Model Checking of Network Protocols in Network Simulators by Exploiting Protocol-Specific Heuristics, Tech. Rep. UIUCDCS-R-2005-2547, Department of Computer Science, University of Illinois at Urbana-Champaign (April 2005)","DOI":"10.1007\/11576280_17"},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Model checking for programming languages using VeriSoft. In: Proc. of ACM POPL 1997 (1997)","DOI":"10.1145\/263699.263717"},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Proc. of ACM POPL 2005 (2005)","DOI":"10.1145\/1040305.1040315"},{"key":"17_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/3-540-46002-0_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Godefroid","year":"2002","unstructured":"Godefroid, P., Khurshid, S.: Exploring very large state spaces using genetic algorithms. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, p. 266. Springer, Heidelberg (2002)"},{"issue":"5","key":"17_CR23","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":"17_CR24","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K. McMillan","year":"1993","unstructured":"McMillan, K.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)"},{"key":"17_CR25","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: Proc. of IEEE ICCD 1992 (1992)","DOI":"10.1109\/ICCD.1992.276232"},{"key":"17_CR26","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":"17_CR27","doi-asserted-by":"crossref","unstructured":"Corbett, J., Dwyer, M., Hatcliff, J., P\u0103s\u0103reanu, C., Robby, Laubach, S., Zheng, H.: Bandera: Extracting finite state models from Java source code. In: Proc. of ICSE (2000)","DOI":"10.1145\/337180.337234"},{"key":"17_CR28","doi-asserted-by":"crossref","unstructured":"Lee, D., Chen, D., Hao, R., Miller, R.E., Wu, J., Yin, X.: A formal approach for passive testing of protocol data portions. In: Proc. of IEEE ICNP 2002 (2002)","DOI":"10.1109\/ICNP.2002.1181393"},{"key":"17_CR29","doi-asserted-by":"crossref","unstructured":"Naumovich, G.N., Clarke, L.A., Osterweil, L.J.: Verification of communication protocols using data flow analysis. In: Proc. of ACM SIGSOFT 1996 (1996)","DOI":"10.1145\/239098.239114"},{"key":"17_CR30","doi-asserted-by":"crossref","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S.: Model checking programs. In: Proc. of IEEE ASE 2000 (2000)","DOI":"10.1109\/ASE.2000.873645"},{"key":"17_CR31","doi-asserted-by":"crossref","unstructured":"Tan, J., Avrunin, G.S., Clarke, L.A., Zilberstein, S., Leue, S.: Heuristic-guided counterexample search in FLAVERS. In: Proc. of ACM SIGSOFT 2004\/FSE-12 (2004)","DOI":"10.1145\/1029894.1029922"},{"key":"17_CR32","doi-asserted-by":"crossref","unstructured":"Yang, C.H., Dill, D.L.: Validation with guided search of the state space. In: Proc. of ACM\/IEE DAC 1998 (1998)","DOI":"10.1145\/277044.277201"},{"issue":"4","key":"17_CR33","doi-asserted-by":"crossref","first-page":"260","DOI":"10.1007\/s10009-003-0130-9","volume":"6","author":"A. Groce","year":"2004","unstructured":"Groce, A., Visser, W.: Heuristics for Model Checking Java Programs. International Journal on Software Tools for Technology Transfer (STTT)\u00a06(4), 260\u2013276 (2004)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11576280_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T14:59:32Z","timestamp":1605625172000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11576280_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540297970","9783540322504"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/11576280_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}