{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T12:01:45Z","timestamp":1763726505043},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642214233"},{"type":"electronic","value":"9783642214240"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-21424-0_14","type":"book-chapter","created":{"date-parts":[[2011,6,15]],"date-time":"2011-06-15T11:52:47Z","timestamp":1308138767000},"page":"173-184","source":"Crossref","is-referenced-by-count":1,"title":["Generating Optimised and Formally Checked Packet Parsing Code"],"prefix":"10.1007","author":[{"given":"Sebastien","family":"Mondet","sequence":"first","affiliation":[]},{"given":"Ion","family":"Alberdi","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Plagemann","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1109\/NSS.2010.44","volume-title":"NSS 2010: Proceedings of the 4th International Conference on Network and System Security","author":"I. Alberdi","year":"2010","unstructured":"Alberdi, I., Owezarski, P., Nicomette, V.: Luth: composing and parallelizing midpoint inspection devices. In: NSS 2010: Proceedings of the 4th International Conference on Network and System Security, pp. 9\u201316. IEEE Computer Society, Melbourne (September 2010)"},{"key":"14_CR2","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1145\/1108792.1108813","volume-title":"PASTE 2005: Proceedings of the 6th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. In: PASTE 2005: Proceedings of the 6th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, pp. 82\u201387. ACM, New York (2005)"},{"key":"14_CR3","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1145\/316188.316214","volume-title":"SIGCOMM 1999: Proceedings of the Conference on Applications, Technologies, Architectures, and Protocols for Computer Communication","author":"A. Begel","year":"1999","unstructured":"Begel, A., McCanne, S., Graham, S.L.: Bpf+: exploiting global data-flow optimization in a generalized packet filter architecture. In: SIGCOMM 1999: Proceedings of the Conference on Applications, Technologies, Architectures, and Protocols for Computer Communication, pp. 123\u2013134. ACM, New York (1999)"},{"key":"14_CR4","unstructured":"Borisov, N., Brumley, D., Wang, H.J., Dunagan, J., Joshi, P., Guo, C.: Generic application-level protocol analyzer and its language. In: NDSS (2007)"},{"key":"14_CR5","unstructured":"Bos, H., de Bruijn, W., Cristea, M., Nguyen, T., Portokalidis, G.: FFPF: Fairly Fast Packet Filters. In: OSDI 2004: Proceedings of the 6th Conference on Symposium on Opearting Systems Design and Implementation (2004)"},{"key":"14_CR6","unstructured":"Chlipala, A.: Certified Programming with Dependent Types. Online in-progress textbook (2009)"},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"Chu, D., Popa, L., Tavakoli, A., Hellerstein, J., Levis, P., Shenker, S., Stoica, I.: The design and implementation of a declarative sensor network system. In: Proceedings of the 5th International Conference on Embedded Networked Sensor Systems (2007)","DOI":"10.1145\/1322263.1322281"},{"key":"14_CR8","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1145\/1345169.1345176","volume-title":"AFM 2007: Proceedings of the Second Workshop on Automated Formal Methods","author":"S. Conchon","year":"2007","unstructured":"Conchon, S., Contejean, E., Kanig, J., Lescuyer, S.: Lightweight integration of the ergo theorem prover inside a proof assistant. In: AFM 2007: Proceedings of the Second Workshop on Automated Formal Methods, pp. 55\u201359. ACM, New York (2007)"},{"issue":"4","key":"14_CR9","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1017\/S095679680200446X","volume":"13","author":"J.C. Filli\u00e2tre","year":"2003","unstructured":"Filli\u00e2tre, J.C.: Verification of non-functional programs using interpretations in type theory. J. Funct. Program.\u00a013(4), 709\u2013745 (2003)","journal-title":"J. Funct. Program."},{"key":"14_CR10","unstructured":"Filli\u00e2tre, J.: Why: A Multi-Language Multi-Prover Verification Tool. Research Report 1366, LRI, Universit\u00e9 Paris Sud (2003)"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Frigo, M.: A fast Fourier transform compiler. ACM SIGPLAN Notices\u00a034(5) (1999)","DOI":"10.1145\/301631.301661"},{"key":"14_CR12","unstructured":"Leroy, X.: Mechanized semantics. In: Logics and Languages for Reliability and Security. NATO Science for Peace and Security Series D: Information and Communication Security, vol.\u00a025, pp. 195\u2013224. IOS Press, Amsterdam"},{"issue":"7","key":"14_CR13","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X. Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM\u00a052(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Madhavapeddy, A.: Combining Static Model Checking with Dynamic Enforcement using the Statecall Policy Language. In: International Conference on Formal Engineering Methods (2009)","DOI":"10.1007\/978-3-642-10373-5_23"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Madhavapeddy, A., Ho, A., Deegan, T., Scott, D., Sohan, R.: Melange: Towards a functional Internet. In: Proceedings of the 2nd ACM SIGOPS\/EuroSys European Conference on Computer Systems (2007)","DOI":"10.1145\/1272996.1273009"},{"key":"14_CR16","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1145\/1596550.1596582","volume-title":"ICFP 2009: Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming","author":"B. Pagano","year":"2009","unstructured":"Pagano, B., Andrieu, O., Moniot, T., Canou, B., Chailloux, E., Wang, P., Manoury, P., Cola\u00e7o, J.L.: Experience report: using Objective Caml to develop safety-critical embedded tools in a certification framework. In: ICFP 2009: Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming, pp. 215\u2013220. ACM, New York (2009)"},{"key":"14_CR17","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1145\/1177080.1177119","volume-title":"IMC 2006: Proceedings of the 6th ACM SIGCOMM Conference on Internet Measurement","author":"R. Pang","year":"2006","unstructured":"Pang, R., Paxson, V., Sommer, R., Peterson, L.: binpac: a yacc for writing application protocol parsers. In: IMC 2006: Proceedings of the 6th ACM SIGCOMM Conference on Internet Measurement, pp. 289\u2013300. ACM, New York (2006)"},{"key":"14_CR18","unstructured":"SANS Institute: Top 20 internet security problems, threats and risks. section 5 anti-virus software (2007), http:\/\/www.sans.org\/top20\/2007\/#s5"},{"key":"14_CR19","unstructured":"Snort Team: Snort Users Manual. The official documentation produced by the Snort team at Sourcefire (2010)"}],"container-title":["IFIP Advances in Information and Communication Technology","Future Challenges in Security and Privacy for Academia and Industry"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21424-0_14.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T03:03:31Z","timestamp":1606187011000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21424-0_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642214233","9783642214240"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21424-0_14","relation":{},"ISSN":["1868-4238","1861-2288"],"issn-type":[{"type":"print","value":"1868-4238"},{"type":"electronic","value":"1861-2288"}],"subject":[],"published":{"date-parts":[[2011]]}}}