{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T16:49:34Z","timestamp":1760028574980},"reference-count":50,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"7","license":[{"start":{"date-parts":[[2014,7,1]],"date-time":"2014-07-01T00:00:00Z","timestamp":1404172800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/3.0\/legalcode"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IIEEE Trans. Software Eng."],"published-print":{"date-parts":[[2014,7,1]]},"DOI":"10.1109\/tse.2014.2323977","type":"journal-article","created":{"date-parts":[[2014,5,14]],"date-time":"2014-05-14T18:01:51Z","timestamp":1400090511000},"page":"695-709","source":"Crossref","is-referenced-by-count":32,"title":["&lt;sc&gt;SymbexNet&lt;\/sc&gt;: Testing Network Protocol Implementations with Symbolic Execution and Rule-Based Specifications"],"prefix":"10.1109","volume":"40","author":[{"family":"JaeSeung Song","sequence":"first","affiliation":[]},{"given":"Cristian","family":"Cadar","sequence":"additional","affiliation":[]},{"given":"Peter","family":"Pietzuch","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref39","first-page":"4:1","author":"schultz-m\u00f8ller","year":"0","journal-title":"Proc 3rd ACM Int Conf Distrib Event-Based Syst"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1145\/1791212.1791235"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1088\/0967-1846\/4\/2\/004"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2007.41"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1145\/1363686.1364148"},{"key":"ref30","first-page":"423","article-title":"D3S: Debugging deployed distributed systems","author":"liu","year":"0"},{"key":"ref37","first-page":"229","article-title":"Snort&#x2014;Lightweight intrusion detection for networks","author":"roesch","year":"0","journal-title":"Proc USENIX Syst Admin Conf"},{"key":"ref36","author":"mockapetris","year":"1987","journal-title":"IETF RFC 1034 Domain Names&#x2014;Concepts and facilities"},{"key":"ref35","first-page":"155","article-title":"Model checking large network protocol implementations","author":"musuvathi","year":"2004","journal-title":"Proc 1st Conf Symp Netw Syst Des Implementation"},{"key":"ref34","first-page":"716","article-title":"Make test-zesti: A symbolic execution solution for improving regression testing","author":"marinescu","year":"0","journal-title":"Proc 34th Int'l Conf Software Eng"},{"key":"ref28","year":"1994"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2004.1281665"},{"key":"ref29","author":"license","year":"0"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44585-4_15"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.17487\/rfc2132"},{"key":"ref20","year":"2004","journal-title":"ISC DHCP"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1145\/1287624.1287710"},{"key":"ref21","first-page":"145","article-title":"Modeling and formal verification of DHCP using SPIN","volume":"3","author":"islam","year":"2006","journal-title":"Int J Comput Sci Appl"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1109\/RELDIS.2004.1353000"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1016\/S1389-1286(00)00005-0"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1016\/S0140-3664(99)00223-6"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-92995-6_5"},{"key":"ref10","author":"cheshire","year":"2010","journal-title":"Multicast DNS (IETF Internet-Draft)"},{"key":"ref11","author":"cheshire","year":"0"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1016\/S1389-1286(03)00316-5"},{"key":"ref12","author":"kaminsky","year":"2008","journal-title":"Black Ops 2008&#x2014;Its the end of the cache as we know it Black Hat USA"},{"key":"ref13","author":"dill","year":"2002","journal-title":"Udhcp client\/server package (2002)"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.17487\/rfc2131"},{"key":"ref15","article-title":"Practical applications of probabilistic model checking to communication protocols","author":"duflot","year":"2010","journal-title":"Handbook of Formal Methods in Industrial Critical Systems"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/972374.972390"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"ref18","first-page":"151","article-title":"Automated whitebox fuzz testing","author":"godefroid","year":"0","journal-title":"Proc Symp Netw Distrib Syst Security"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2004.836136"},{"key":"ref4","author":"bradner","year":"1996","journal-title":"IETF RFC 2026 The internet standards process&#x2014;Revision 3"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2004.1348045"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/1247480.1247620"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.17487\/rfc2119"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/1180405.1180445"},{"key":"ref7","first-page":"209","article-title":"KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs","author":"cadar","year":"0","journal-title":"Proc 8th USENIX Conf Operating Systems Design and Implementation"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1109\/SECPRI.2001.924296"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985995"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2007.05.007"},{"key":"ref45","author":"tanenbaum","year":"2002","journal-title":"Computer Networks"},{"key":"ref48","author":"vitkovsky","year":"2009","journal-title":"dhquery"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1109\/MCOM.2007.4342835"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1109\/ICCCN.2011.6005945"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1145\/350887.350891"},{"key":"ref44","author":"steinberg","year":"2005"},{"key":"ref43","first-page":"582","article-title":"Towards automated verification of autonomous networks: A case study in self-configuration","author":"song","year":"0"}],"container-title":["IEEE Transactions on Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/32\/6848876\/06815719.pdf?arnumber=6815719","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T16:53:06Z","timestamp":1642006386000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6815719\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,7,1]]},"references-count":50,"journal-issue":{"issue":"7"},"URL":"https:\/\/doi.org\/10.1109\/tse.2014.2323977","relation":{},"ISSN":["0098-5589","1939-3520"],"issn-type":[{"value":"0098-5589","type":"print"},{"value":"1939-3520","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,7,1]]}}}