{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T05:31:06Z","timestamp":1725514266141},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540688624"},{"type":"electronic","value":"9783540688631"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-68863-1_14","type":"book-chapter","created":{"date-parts":[[2008,6,2]],"date-time":"2008-06-02T07:20:45Z","timestamp":1212391245000},"page":"220-239","source":"Crossref","is-referenced-by-count":15,"title":["VeriCool: An Automatic Verifier for a Concurrent Object-Oriented Language"],"prefix":"10.1007","author":[{"given":"Jan","family":"Smans","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bart","family":"Jacobs","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frank","family":"Piessens","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"14_CR1","unstructured":"Gosling, J., Joy, B., Steele, G., Bracha, G.: The java language specification, 3rd edn. (2005)"},{"key":"14_CR2","unstructured":"Jacobs, B., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. In: SAVCBS (2004)"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Leino, K.R.M., Piessens, F., Schulte, W.: Safe concurrency for aggregate objects with invariants. In: SEFM (2005)","DOI":"10.1109\/SEFM.2005.39"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Smans, J., Piessens, F., Schulte, W.: A statically verifiable programming model for concurrent object-oriented programs. In: ICFEM (2006)","DOI":"10.1007\/11901433_23"},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"Smans, J., Jacobs, B., Piessens, F., Schulte, W.: An automatic verifier for java-like programs based on dynamic frames (2008)","DOI":"10.1007\/978-3-540-78743-3_19"},{"key":"14_CR6","unstructured":"Kassios, Y.: A Theory of Object Oriented Refinement. PhD thesis, University of Toronto (2006)"},{"key":"14_CR7","unstructured":"http:\/\/www.cs.kuleuven.be\/~jans\/vericool"},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"Hobor, A., Appel, A.W., Nardelli, F.Z.: Oracle semantics for concurrent separation logic. In: ESOP (2008)","DOI":"10.1007\/978-3-540-78739-6_27"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency and local reasoning. Theoretical Computer Science\u00a0375(1-3) (2007)","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Gotsman, A., Berdine, J., Cook, B., Rinetzky, N., Sagiv, M.: Local reasoning for storable locks and threads. In: APLAS (2007)","DOI":"10.1007\/978-3-540-76637-7_3"},{"key":"14_CR11","unstructured":"Haack, C., Hurlin, C.: Separation logic contracts for a java-like language with fork\/join. Technical Report 6430, INRIA (2008)"},{"key":"14_CR12","unstructured":"DeLine, R., Leino, K.R.M.: Boogiepl: A typed procedural language for checking object-oriented programs. Technical Report MSR-TR-, -70 (2005)"},{"key":"14_CR13","unstructured":"Leino, K.R.M., Schulte, W.: A verifying compiler for a multi-threaded object-oriented language. In: Marktoberdorf Summer School Lecture Notes (2006)"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for java. In: PLDI (2002)","DOI":"10.1145\/512529.512558"},{"key":"14_CR15","unstructured":"Leino, K.R.M., Nelson, G., Saxe, J.B.: Esc\/java user\u2019s manual. Technical Report SRC-TN-2000-002, Compaq Research Center (2000)"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Parkinson, M., Vafeiadis, V.: Modular safety checking for fine-grained concurrency. In: SAS (2007)","DOI":"10.1007\/978-3-540-74061-2_15"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Smallfoot: Modular automatic assertion checking with separation logic. In: FMCO (2005)","DOI":"10.1007\/11804192_6"},{"key":"14_CR18","series-title":"Lecture Notes in Computer Science","volume-title":"Foundations of Software Science and Computation Structures","author":"E. \u00c1brah\u00e1m Mumm","year":"2002","unstructured":"\u00c1brah\u00e1m Mumm, E., de Boer, F.S., de Roever, W.P., Steffen, M.: Verification for java\u2019s reentrant multithreading concept. In: Nielsen, M., Engberg, U. (eds.) ETAPS 2002 and FOSSACS 2002. LNCS, vol.\u00a02303, Springer, Heidelberg (2002)"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Boyapati, C., Lee, R., Rinard, M.: Ownership types for safe programming: Preventing data races and deadlocks. In: OOPSLA (2002)","DOI":"10.1145\/582419.582440"},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"Hoare, C.: Monitors: An operating system structuring concept. cacm 17(10) (1974)","DOI":"10.1145\/355620.361161"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Open Object-Based Distributed Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-68863-1_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,6]],"date-time":"2020-05-06T02:54:03Z","timestamp":1588733643000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-68863-1_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540688624","9783540688631"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-68863-1_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}