{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:44:12Z","timestamp":1725493452750},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540007081"},{"type":"electronic","value":"9783540365327"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36532-x_14","type":"book-chapter","created":{"date-parts":[[2007,10,25]],"date-time":"2007-10-25T15:34:36Z","timestamp":1193326476000},"page":"217-233","source":"Crossref","is-referenced-by-count":6,"title":["Formalization and Verification of a Mail Server in Coq"],"prefix":"10.1007","author":[{"given":"Reynald","family":"Affeldt","sequence":"first","affiliation":[]},{"given":"Naoki","family":"Kobayashi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,6,25]]},"reference":[{"key":"14_CR1","unstructured":"D. Bernstein and various contributors. The qmail home page. http:\/\/www.qmail.org."},{"key":"14_CR2","unstructured":"Y. Bertot. A certified compiler for an imperative language. Technical Report RR-3488, INRIA, Sep. 1998."},{"key":"14_CR3","unstructured":"P. E. Black. Axiomatic Semantics Verification of a Secure Web Server. PhD thesis, Department of Computer Science, Brigham Young University, Feb. 1998."},{"key":"14_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1007\/BFb0105396","volume-title":"Theorem Proving in Higher Order Logics","author":"P. E. Black","year":"1996","unstructured":"P. E. Black and P. J. Windley. Inference rules for programming languages with side effects in expressions. In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics, volume 1125 of Lecture Notes in Computer Science, pages 51\u201360. Springer-Verlag, August 1996."},{"issue":"5","key":"14_CR5","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E. M. Clarke","year":"1994","unstructured":"E. M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. ACM ransactions on Programming Languages and Systems, 16(5):1512\u20131542, September 1994.","journal-title":"ACM ransactions on Programming Languages and Systems"},{"issue":"4","key":"14_CR6","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1145\/242223.242257","volume":"28","author":"E. M. Clarke","year":"1996","unstructured":"E. M. Clarke and J. M. Wing. Formal methods: state of the art and future directions. ACM Computing Surveys, 28(4):626\u2013643, 1996.","journal-title":"ACM Computing Surveys"},{"key":"14_CR7","unstructured":"F. B. Cohen. Why is thttpd secure? Available at http:\/\/www.all.net\/journal\/white\/whitepaper.html."},{"key":"14_CR8","series-title":"Lect Notes Comput Sci","first-page":"331","volume-title":"Theorem Proving in Higher Order Logics","author":"T. N. Nazareth Dieter","year":"1996","unstructured":"T. N. Dieter Nazareth. Formal verification of algorithm W: The monomorphic case. In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics, volume 1125 of Lecture Notes in Computer Science, pages 331\u2013345. Springer-Verlag, Aug. 1996."},{"key":"14_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/BFb0028390","volume-title":"Theorem Proving in Higher Order Logics","author":"B. Dutertre","year":"1997","unstructured":"B. Dutertre and S. Schneider. Using a PVS embedding of CSP to verify authentication protocols. In A. F. Elsa L. Gunter, editor, Theorem Proving in Higher Order Logics, volume 1275 of Lecture Notes in Computer Science, pages 121\u2013136. Springer-Verlag, Aug. 1997."},{"key":"14_CR10","unstructured":"J.-C. Filli\u00e2tre. Preuve de programmes imp\u00e9ratifs en th\u00e9orie des types. PhD thesis, Universit\u00e9 Paris-Sud, Jul. 1999. Available at http:\/\/www.lri.fr\/~filliatr\/ftp\/publis\/these.ps.gz."},{"key":"14_CR11","unstructured":"B. C. Pierce and J. Vouillon. Specifying a file synchronizer (full version). Draft, Mar. 2002."},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"J. B. Postel. Rfc 821: Simple mail transfer protocol. Available at http:\/\/www.faqs.org\/rfcs\/rfc821.html , Aug. 1982.","DOI":"10.17487\/rfc0821"},{"key":"14_CR13","series-title":"Lect Notes Comput Sci","volume-title":"AnZenMail: A secure and certified e-mail system","author":"E. Shibayama","year":"2003","unstructured":"E. Shibayama, S. Hagihara, N. Kobayashi, S. Nishizaki, K. Taura, and T. Watanabe. AnZenMail: A secure and certified e-mail system. In M. Okada, B. Pierce, A. Scedrov, H. Tokuda, and A. Yonezawa, editors, Proceedings of International Symposium on Software Security, Keio University, Tokyo, Japan (Nov. 2002), Lecture Notes in Computer Science. Springer-Verlag, Feb. 2003."},{"key":"14_CR14","unstructured":"The Coq Development Team. The Coq proof assistant reference manual. Available at http:\/\/coq.inria.fr\/doc\/main.html , 2002."},{"key":"14_CR15","unstructured":"P. Wadler. Monads for functional programming. In M. Broy, editor, Marktoberdorf Summer School on Program Design Calculi, volume 118 of NATO ASI Series F: Computer and systems sciences. Springer-Verlag, Aug. 1992. Also in J. Jeuring and E. Meijer, editors, Advanced Functional Programming, Springer Verlag, LNCS 925, 1995. Some errata fixed August 2001."}],"container-title":["Lecture Notes in Computer Science","Software Security \u2014 Theories and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36532-X_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T20:54:24Z","timestamp":1556916864000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36532-X_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540007081","9783540365327"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-36532-x_14","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}