{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:48:53Z","timestamp":1740098933432,"version":"3.37.3"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319668444"},{"type":"electronic","value":"9783319668451"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66845-1_26","type":"book-chapter","created":{"date-parts":[[2017,8,26]],"date-time":"2017-08-26T15:37:20Z","timestamp":1503761840000},"page":"391-406","source":"Crossref","is-referenced-by-count":4,"title":["Formal Verification of ARP (Address Resolution Protocol) Through SMT-Based Model Checking - A Case Study -"],"prefix":"10.1007","author":[{"given":"Danilo","family":"Bruschi","sequence":"first","affiliation":[]},{"given":"Andrea","family":"Di Pasquale","sequence":"additional","affiliation":[]},{"given":"Silvio","family":"Ghilardi","sequence":"additional","affiliation":[]},{"given":"Andrea","family":"Lanzi","sequence":"additional","affiliation":[]},{"given":"Elena","family":"Pagani","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,27]]},"reference":[{"key":"26_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1007\/978-3-540-71209-1_56","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PA Abdulla","year":"2007","unstructured":"Abdulla, P.A., Delzanno, G., Henda, N.B., Rezine, A.: Regular model checking without transducers (on efficient verification of parameterized systems). In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 721\u2013736. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-71209-1_56"},{"key":"26_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/978-3-642-35873-9_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"PA Abdulla","year":"2013","unstructured":"Abdulla, P.A., Haziza, F., Hol\u00edk, L.: All for the price of few. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 476\u2013495. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-35873-9_28"},{"key":"26_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-540-28644-8_3","volume-title":"CONCUR 2004 - Concurrency Theory","author":"PA Abdulla","year":"2004","unstructured":"Abdulla, P.A., Jonsson, B., Nilsson, M., Saksena, M.: A survey of regular model checking. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 35\u201348. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-28644-8_3"},{"key":"26_CR4","unstructured":"Alqahtani, A.H., Iftikhar, M.: TCP\/IP attacks, defenses and security tools. Int. J. Sci. Mod. Eng. (IJISME) 1(10) (2013)"},{"key":"26_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1007\/11562948_35","volume-title":"Automated Technology for Verification and Analysis","author":"S Bardin","year":"2005","unstructured":"Bardin, S., Finkel, A., Leroux, J., Schnoebelen, P.: Flat acceleration in symbolic model checking. In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol. 3707, pp. 474\u2013488. Springer, Heidelberg (2005). doi: 10.1007\/11562948_35"},{"issue":"2","key":"26_CR6","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1145\/378444.378449","volume":"19","author":"SM Bellovin","year":"1989","unstructured":"Bellovin, S.M.: Security problems in the TCP\/IP protocol suite. ACM SIGCOMM Comput. Commun. Rev. 19(2), 32\u201348 (1989)","journal-title":"ACM SIGCOMM Comput. Commun. Rev."},{"issue":"4","key":"26_CR7","doi-asserted-by":"crossref","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. J. ACM 49(4), 538\u2013576 (2002)","journal-title":"J. ACM"},{"key":"26_CR8","series-title":"Synthesis Lectures on Distributed Computing Theory","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-031-02011-7","volume-title":"Decidability of Parameterized Verification","author":"R Bloem","year":"2015","unstructured":"Bloem, R., Jacobs, S., Khalimov, A., Konnov, I., Rubin, S., Veith, H., Widder, J.: Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, San Rafael (2015)"},{"key":"26_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-540-27813-9_29","volume-title":"Computer Aided Verification","author":"A Bouajjani","year":"2004","unstructured":"Bouajjani, A., Habermehl, P., Vojnar, T.: Abstract regular model checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 372\u2013386. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-27813-9_29"},{"key":"26_CR10","doi-asserted-by":"crossref","unstructured":"Cheshire, S.: IPv4 Address Conflict Detection. RFC 5227, July 2008","DOI":"10.17487\/rfc5227"},{"key":"26_CR11","doi-asserted-by":"crossref","unstructured":"Cheshire, S., Aboba, B., Guttman, E.: Dynamic Configuration of IPv4 Link-Local Addresses. RFC 3927, May 2005","DOI":"10.17487\/rfc3927"},{"key":"26_CR12","doi-asserted-by":"crossref","unstructured":"Conchon, S., Goel, A., Krstic, S., Mebsout, A., Za\u00efdi, F.: Invariants for finite instances and beyond. In: Proceedings of FMCAD (2013)","DOI":"10.1109\/FMCAD.2013.6679392"},{"key":"26_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"718","DOI":"10.1007\/978-3-642-31424-7_55","volume-title":"Computer Aided Verification","author":"S Conchon","year":"2012","unstructured":"Conchon, S., Goel, A., Krsti\u0107, S., Mebsout, A., Za\u00efdi, F.: Cubicle: a parallel SMT-based model checker for parameterized systems. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 718\u2013724. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31424-7_55"},{"key":"26_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-540-71070-7_6","volume-title":"Automated Reasoning","author":"S Ghilardi","year":"2008","unstructured":"Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Towards SMT model checking of array-based systems. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 67\u201382. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-71070-7_6"},{"key":"26_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-642-14203-1_3","volume-title":"Automated Reasoning","author":"S Ghilardi","year":"2010","unstructured":"Ghilardi, S., Ranise, S.: MCMT: a model checker modulo theories. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 22\u201329. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-14203-1_3"},{"key":"26_CR16","doi-asserted-by":"crossref","unstructured":"Ghilardi, S., Ranise, S.: Backward reachability of array-based systems by SMT solving: termination and invariant synthesis. J. Log. Methods Comput. Sci. 6(4) (2010)","DOI":"10.2168\/LMCS-6(4:10)2010"},{"issue":"6","key":"26_CR17","first-page":"145","volume":"3","author":"SMS Islam","year":"2006","unstructured":"Islam, S.M.S., Sqalli, M.S., Khan, S.: Modeling and formal verification of DHCP using SPIN. Int. J. Comput. Sci. Appl. 3(6), 145\u2013159 (2006)","journal-title":"Int. J. Comput. Sci. Appl."},{"key":"26_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/3-540-15216-4_15","volume-title":"Distributed Systems","author":"MW Alford","year":"1985","unstructured":"Alford, M.W., Ansart, J.P., Hommel, G., Lamport, L., Liskov, B., Mullery, G.P., Schneider, F.B.: Formal foundation for specification and verification. In: Paul, M., et al. (eds.) Distributed Systems. LNCS, vol. 190, pp. 203\u2013285. Springer, Heidelberg (1985). doi: 10.1007\/3-540-15216-4_15"},{"key":"26_CR19","doi-asserted-by":"crossref","unstructured":"Plummer, D.C.: An Ethernet Address Resolution Protocol - or - Converting Network Protocol Addresses to 48.bit Ethernet Address for Transmission on Ethernet Hardware. RFC 826, November 1982","DOI":"10.17487\/rfc0826"},{"key":"26_CR20","volume-title":"Address Resolution Protocol Spoofing and Man-in-the-Middle Attacks","author":"R Wagner","year":"2001","unstructured":"Wagner, R.: Address Resolution Protocol Spoofing and Man-in-the-Middle Attacks. The SANS Institute, Reston (2001)"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66845-1_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T20:25:50Z","timestamp":1659385550000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66845-1_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319668444","9783319668451"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66845-1_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}