{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T10:34:32Z","timestamp":1743071672742,"version":"3.40.3"},"publisher-location":"Cham","reference-count":12,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319050317"},{"type":"electronic","value":"9783319050324"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-05032-4_28","type":"book-chapter","created":{"date-parts":[[2014,3,7]],"date-time":"2014-03-07T09:36:26Z","timestamp":1394184986000},"page":"389-404","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Soundness and Completeness of the NRB Verification Logic"],"prefix":"10.1007","author":[{"given":"Peter T.","family":"Breuer","sequence":"first","affiliation":[]},{"given":"Simon J.","family":"Pickin","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,3,8]]},"reference":[{"key":"28_CR1","unstructured":"American National Standards Institute. American national standard for information systems - programming language C, ANSI X3.159-1989 (1989)"},{"issue":"4","key":"28_CR2","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1145\/357146.357150","volume":"3","author":"KR Apt","year":"1981","unstructured":"Apt, K.R.: Ten years of Hoare\u2019s logic: a survey: part I. ACM Trans. Program. Lang. Syst. 3(4), 431\u2013483 (1981)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"2","key":"28_CR3","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/1646353.1646374","volume":"53","author":"A Bessey","year":"2010","unstructured":"Bessey, A., Block, K., Chelf, B., Chou, A., Fulton, B., Hallem, S., Henri-Gros, C., Kamsky, A., McPeak, S., Engler, D.: A few billion lines of code later: using static analysis to find bugs in the real world. Commun. ACM 53(2), 66\u201375 (2010)","journal-title":"Commun. ACM"},{"key":"28_CR4","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"765","DOI":"10.1007\/11758549_103","volume-title":"ICCS 2006","author":"PT Breuer","year":"2006","unstructured":"Breuer, P.T., Pickin, S.: Checking for deadlock, double-free and other abuses in the Linux kernel source code. In: Alexandrov, V.N., van Albada, G.D., Sloot, P.M.A., Dongarra, J. (eds.) ICCS 2006. LNCS, vol. 3994, pp. 765\u2013772. Springer, Heidelberg (2006)"},{"key":"28_CR5","series-title":"LNCS","first-page":"52","volume-title":"Ada-Europe 2004","author":"PT Breuer","year":"2004","unstructured":"Breuer, P.T., Valls, M.: Static deadlock detection in the Linux kernel. In: Llamos\u00ed, A., Strohmeier, A. (eds.) Ada-Europe 2004. LNCS, vol. 3063, pp. 52\u201364. Springer, Heidelberg (2004)"},{"issue":"3","key":"28_CR6","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/s11334-006-0010-z","volume":"2","author":"PT Breuer","year":"2006","unstructured":"Breuer, P.T., Pickin, S.: Symbolic approximation: an approach to verification in the large. Innovations Syst. Softw. Eng. 2(3), 147\u2013163 (2006)","journal-title":"Innovations Syst. Softw. Eng."},{"key":"28_CR7","doi-asserted-by":"crossref","unstructured":"Breuer, P.T., Pickin, S.: Verification in the large via symbolic approximation. In: Proceedings of the 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, 2006 (ISoLA 2006), pp. 408\u2013415. IEEE (2006)","DOI":"10.1109\/ISoLA.2006.20"},{"key":"28_CR8","doi-asserted-by":"publisher","unstructured":"Breuer, P.T., Pickin, S.: Open source verification in an anonymous volunteer network. Sci. Comput. Program. (2013). doi: 10.1016\/j.scico.2013.08.010","DOI":"10.1016\/j.scico.2013.08.010"},{"key":"28_CR9","doi-asserted-by":"crossref","unstructured":"Breuer, P.T., Pickin, S., Petrie, M.L.: Detecting deadlock, double-free and other abuses in a million lines of Linux kernel source. In: Proceedings of the 30th Annual Software Engineering Workshop 2006 (SEW\u201906), pp. 223\u2013233. IEEE\/NASA (2006)","DOI":"10.1109\/SEW.2006.15"},{"issue":"2","key":"28_CR10","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E Clarke","year":"1986","unstructured":"Clarke, E., Emerson, E., Sistla, A.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Prog. Lang. Syst. (TOPLAS) 8(2), 244\u2013253 (1986)","journal-title":"ACM Trans. Prog. Lang. Syst. (TOPLAS)"},{"key":"28_CR11","doi-asserted-by":"crossref","unstructured":"Engler, D., Chelf, B., Chou, A., Hallem, S.: Checking system rules using system-specific, programmer-written compiler extensions. In: Proceedings of the 4th Symposium on Operating System Design and Implementation (OSDI 2000), pp. 1\u201316, October 2000","DOI":"10.21236\/ADA419626"},{"key":"28_CR12","unstructured":"International Standards Organisation. ISO\/IEC 9899-1999, programming languages - C (1999)"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-05032-4_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,19]],"date-time":"2023-02-19T22:48:23Z","timestamp":1676846903000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-05032-4_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319050317","9783319050324"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-05032-4_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"8 March 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}