{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T15:21:01Z","timestamp":1725895261338},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642104510"},{"type":"electronic","value":"9783642104527"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-10452-7_18","type":"book-chapter","created":{"date-parts":[[2009,11,4]],"date-time":"2009-11-04T08:37:26Z","timestamp":1257323846000},"page":"266-281","source":"Crossref","is-referenced-by-count":5,"title":["Low-Level Code Verification Based on CSP Models"],"prefix":"10.1007","author":[{"given":"Moritz","family":"Kleine","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Steffen","family":"Helke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"18_CR1","unstructured":"FDR2 User Manual (2005), \n                  \n                    http:\/\/www.fsel.com\/documentation\/fdr2\/"},{"key":"18_CR2","unstructured":"ProB Manual (2005), \n                  \n                    http:\/\/www.stups.uni-duesseldorf.de\/ProB\/"},{"key":"18_CR3","unstructured":"Barrett, G.: occam 3 Reference Manual. Inmos Ltd. (1992)"},{"key":"18_CR4","unstructured":"G\u00f6thel, T., Glesner, S.: Machine Checkable Timed CSP. In: The First NASA Formal Methods Symposium (2009)"},{"key":"18_CR5","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall Int., Englewood Cliffs (1985)"},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"108","DOI":"10.1007\/978-3-540-31980-1_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y. Isobe","year":"2005","unstructured":"Isobe, Y., Roggenbach, M.: A generic theorem prover of CSP refinement. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 108\u2013123. Springer, Heidelberg (2005)"},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"Lattner, C., Adve, V.: Automatic pool allocation for disjoint data structures. In: ACM SIGPLAN Workshop on Memory System Performance, Germany (2002)","DOI":"10.1145\/773146.773041"},{"key":"18_CR8","unstructured":"LLVM Reference Manual (2008), \n                  \n                    http:\/\/llvm.org\/docs\/LangRef.html"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/3-540-45251-6_6","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"M. Leuschel","year":"2001","unstructured":"Leuschel, M., Massart, T., Currie, A.: How to make FDR Spin: LTL model checking of CSP using refinement. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol.\u00a02021, p. 99. Springer, Heidelberg (2001)"},{"key":"18_CR10","unstructured":"Montenegro, S., Briess, K., Kayal, H.: Dependable Software (BOSS) for the BEESAT pico satellite. In: DASIA 2006 - Data Systems In Aerospace, Germany (2006)"},{"key":"18_CR11","unstructured":"Oechslein, B.: Statische WCET Analyse von LLVM Bytecode. Master\u2019s thesis, Universit\u00e4t Erlangen (2008)"},{"key":"18_CR12","volume-title":"The Theory and Practice of Concurrency","author":"A.W. Roscoe","year":"1997","unstructured":"Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall PTR, Upper Saddle River (1997)"},{"key":"18_CR13","unstructured":"Scattergood, B.: The semantics and implementation of machine-readable CSP PhD thesis, University of Oxford (1998)"},{"issue":"11","key":"18_CR14","first-page":"1277","volume":"9","author":"F. Scuglik","year":"2003","unstructured":"Scuglik, F., Sveda, M.: Automatically generated CSP specifications. Journal of Universal Computer Science\u00a09(11), 1277\u20131295 (2003)","journal-title":"Journal of Universal Computer Science"},{"key":"18_CR15","unstructured":"Shi, H.: Java2CSP: A system for verifying concurrent Java programs. In: Workshop on Tools for System Design and Verification (FM-TOOLS), Ulmer Informatik-Berichte (2000)"},{"key":"18_CR16","first-page":"32","volume-title":"Int. Symposium on Principles of programming languages (POPL)","author":"B. Steensgaard","year":"1996","unstructured":"Steensgaard, B.: Points-to analysis in almost linear time. In: Int. Symposium on Principles of programming languages (POPL), pp. 32\u201341. ACM, New York (1996)"},{"key":"18_CR17","first-page":"1","volume-title":"Aerospace Conference","author":"S. Thompson","year":"2008","unstructured":"Thompson, S., Brat, G.: Verification of C++ Flight Software with the MCP Model Checker. In: Aerospace Conference, pp. 1\u20139. IEEE, Los Alamitos (2008)"},{"key":"18_CR18","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1109\/PDSE.2000.847856","volume-title":"Software Engineering for Parallel and Distributed Systems","author":"P.H. Welch","year":"2000","unstructured":"Welch, P.H., Martin, J.M.R.: A CSP model for Java multithreading. In: Software Engineering for Parallel and Distributed Systems, pp. 114\u2013122. IEEE, Los Alamitos (2000)"},{"key":"18_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-540-85114-1_22","volume-title":"Model Checking Software","author":"A. Zaks","year":"2008","unstructured":"Zaks, A., Joshi, R.: Verifying multi-threaded C programs with Spin. In: Havelund, K., Majumdar, R., Palsberg, J. (eds.) SPIN 2008. LNCS, vol.\u00a05156, pp. 325\u2013342. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Foundations and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-10452-7_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T11:31:45Z","timestamp":1619782305000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-10452-7_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642104510","9783642104527"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-10452-7_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}