{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:04:27Z","timestamp":1770282267916,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642228629","type":"print"},{"value":"9783642228636","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-22863-6_27","type":"book-chapter","created":{"date-parts":[[2011,8,8]],"date-time":"2011-08-08T05:47:55Z","timestamp":1312782475000},"page":"363-369","source":"Crossref","is-referenced-by-count":10,"title":["Lem: A Lightweight Tool for Heavyweight Semantics"],"prefix":"10.1007","author":[{"given":"Scott","family":"Owens","sequence":"first","affiliation":[]},{"given":"Peter","family":"B\u00f6hm","sequence":"additional","affiliation":[]},{"given":"Francesco","family":"Zappa Nardelli","sequence":"additional","affiliation":[]},{"given":"Peter","family":"Sewell","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"27_CR1","unstructured":"ACL2 Version 4.2 (2011), http:\/\/www.cs.utexas.edu\/~moore\/acl2\/"},{"key":"27_CR2","first-page":"55","volume-title":"POPL 2011","author":"M. Batty","year":"2011","unstructured":"Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing C++ concurrency. In: POPL 2011, pp. 55\u201366. ACM, New York (2011)"},{"key":"27_CR3","first-page":"117","volume-title":"ICNP 2006","author":"A. Biltcliffe","year":"2006","unstructured":"Biltcliffe, A., Dales, M., Jansen, S., Ridge, T., Sewell, P.: Rigorous protocol design in practice: An optical packet-switch MAC in HOL. In: ICNP 2006, pp. 117\u2013126. IEEE, Los Alamitos (2006)"},{"key":"27_CR4","first-page":"265","volume-title":"SIGCOMM 2005","author":"S. Bishop","year":"2005","unstructured":"Bishop, S., Fairbairn, M., Norrish, M., Sewell, P., Smith, M., Wansbrough, K.: Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and Sockets. In: SIGCOMM 2005, pp. 265\u2013276. ACM, New York (2005)"},{"key":"27_CR5","volume-title":"PPDP 2011","author":"J.C. Blanchette","year":"2011","unstructured":"Blanchette, J.C., Weber, T., Batty, M., Owens, S., Sarkar, S.: Nitpicking C++ concurrency. In: PPDP 2011. ACM, New York (to appear, 2011)"},{"key":"27_CR6","unstructured":"The Coq proof assistant, v.8.3 (2011), http:\/\/coq.inria.fr\/"},{"key":"27_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-14052-5_18","volume-title":"Interactive Theorem Proving","author":"A. Fox","year":"2010","unstructured":"Fox, A., Myreen, M.O.: A trustworthy monadic formalization of the ARMv7 instruction set architecture. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 243\u2013258. Springer, Heidelberg (2010)"},{"key":"27_CR8","unstructured":"Harrison, J.: HOL Light (2011), http:\/\/www.cl.cam.ac.uk\/~jrh13\/hol-light\/"},{"key":"27_CR9","unstructured":"The HOL 4 system, Kananaskis-6 release (2011), http:\/\/hol.sourceforge.net\/"},{"key":"27_CR10","unstructured":"Isabelle 2011 (2011), http:\/\/isabelle.in.tum.de\/"},{"key":"27_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-78739-6_1","volume-title":"Programming Languages and Systems","author":"S. Owens","year":"2008","unstructured":"Owens, S.: A sound semantics for OCaml $_{\\emph{light}}$ . In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol.\u00a04960, pp. 1\u201315. Springer, Heidelberg (2008)"},{"key":"27_CR12","unstructured":"PVS 5.0 (2011), http:\/\/pvs.csl.sri.com\/"},{"key":"27_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-68237-0_21","volume-title":"FM 2008: Formal Methods","author":"T. Ridge","year":"2008","unstructured":"Ridge, T., Norrish, M., Sewell, P.: A rigorous approach to networking: TCP, from implementation to protocol to service. In: Cuellar, J., Sere, K. (eds.) FM 2008. LNCS, vol.\u00a05014, pp. 294\u2013309. Springer, Heidelberg (2008)"},{"key":"27_CR14","volume-title":"PLDI 2011","author":"S. Sarkar","year":"2011","unstructured":"Sarkar, S., Sewell, P., Alglave, J., Maranget, L., Williams, D.: Understanding POWER multiprocessors. In: PLDI 2011. ACM, New York (to appear, 2011)"},{"key":"27_CR15","first-page":"379","volume-title":"POPL 2009","author":"S. Sarkar","year":"2009","unstructured":"Sarkar, S., Sewell, P., Zappa Nardelli, F., Owens, S., Ridge, T., Braibant, T., Myreen, M.O., Alglave, J.: The semantics of x86 multiprocessor machine code. In: POPL 2009, pp. 379\u2013391. ACM, New York (2009)"},{"key":"27_CR16","first-page":"43","volume-title":"POPL 2011","author":"J. \u0160e\u010d\u00edk","year":"2011","unstructured":"\u0160e\u010d\u00edk, J., Vafeiadis, V., Zappa Nardelli, F., Jagannathan, S., Sewell, P.: Relaxed-memory concurrency and verified compilation. In: POPL 2011, pp. 43\u201354. ACM, New York (2011)"},{"key":"27_CR17","doi-asserted-by":"crossref","unstructured":"Sewell, P., Zappa Nardelli, F., Owens, S., Peskine, G., Ridge, T., Sarkar, S., Strni\u0161a, R.: Ott: Effective tool support for the working semanticist. JFP\u00a020(1) (January 2010)","DOI":"10.1017\/S0956796809990293"},{"key":"27_CR18","first-page":"499","volume-title":"OOPSLA 2007","author":"R. Strni\u0161a","year":"2007","unstructured":"Strni\u0161a, R., Sewell, P., Parkinson, M.: The Java Module System: core design and semantic definition. In: OOPSLA 2007, pp. 499\u2013514. ACM, New York (2007)"},{"key":"27_CR19","unstructured":"Twelf 1.5 (2011), http:\/\/twelf.plparty.org\/wiki\/Main_Page"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22863-6_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,13]],"date-time":"2019-06-13T18:13:45Z","timestamp":1560449625000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22863-6_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642228629","9783642228636"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22863-6_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}