{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:00:31Z","timestamp":1725516031339},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540799795"},{"type":"electronic","value":"9783540799801"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-79980-1_16","type":"book-chapter","created":{"date-parts":[[2008,7,28]],"date-time":"2008-07-28T15:55:42Z","timestamp":1217260542000},"page":"199-215","source":"Crossref","is-referenced-by-count":20,"title":["Separation Logic Contracts for a Java-Like Language with Fork\/Join"],"prefix":"10.1007","author":[{"given":"Christian","family":"Haack","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cl\u00e9ment","family":"Hurlin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Barnett, M., DeLine, R., F\u00e4hndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. Journal of Object Technology\u00a03(6) (2004)","DOI":"10.5381\/jot.2004.3.6.a2"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Smallfoot: Modular automatic assertion checking with separation logic. In: Formal Methods for Components and Objects (2005)","DOI":"10.1007\/11804192_6"},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"Bierhoff, K., Aldrich, J.: Modular typestate verification of aliased objects. In: ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (2007)","DOI":"10.21236\/ADA465507"},{"key":"16_CR4","volume-title":"Principles of Programming Languages","author":"R. Bornat","year":"2005","unstructured":"Bornat, R., O\u2019Hearn, P., Calcagno, C., Parkinson, M.: Permission accounting in separation logic. In: Principles of Programming Languages. ACM Press, New York (2005)"},{"key":"16_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_4","volume-title":"Static Analysis Symposium","author":"J. Boyland","year":"2003","unstructured":"Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694. Springer, Heidelberg (2003)"},{"key":"16_CR6","unstructured":"Boyland, J.: Semantics of fractional permissions with nesting. Technical report, University of Wisconsin at Milwaukee (2007)"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Boyland, J., Retert, W.: Connecting effects and uniqueness with adoption. In: Principles of Programming Languages (2005)","DOI":"10.1145\/1040305.1040329"},{"key":"16_CR8","unstructured":"Boyland, J., Retert, W., Zhao, Y.: Iterators can be independent \u201dfrom\u201d their collections. In: International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (2007)"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"Chin, W., David, C., Nguyen, H., Qin, S.: Enhancing modular OO verification with separation logic. In: Principles of Programming Languages (2008)","DOI":"10.1145\/1328438.1328452"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"Crary, K., Walker, D., Morrisett, G.: Typed memory management in a calculus of capabilities. In: Principles of Programming Languages (1999)","DOI":"10.1145\/292540.292564"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"DeLine, R., F\u00e4hndrich, M.: Enforcing high-level protocols in low-level software. In: Programming Languages Design and Implementation (2001)","DOI":"10.1145\/378795.378811"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"DeLine, R., F\u00e4hndrich, M.: Typestates for objects. In: European Conference on Object-Oriented Programming (2004)","DOI":"10.1007\/978-3-540-24851-4_21"},{"key":"16_CR13","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511629150","volume-title":"Advances in Linear Logic","author":"J.-Y. Girard","year":"1995","unstructured":"Girard, J.-Y.: Linear logic: Its syntax and semantics. In: Girard, J.-Y., Lafont, Y., Regnier, L. (eds.) Advances in Linear Logic. Cambridge University Press, Cambridge (1995)"},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"Gotsman, A., Berdine, J., Cook, B., Rinetzky, N., Sagiv, M.: Local reasoning for storable locks and threads. In: Asian Programming Languages and Systems Symposium (2007)","DOI":"10.1007\/978-3-540-76637-7_3"},{"key":"16_CR15","unstructured":"Haack, C., Hurlin, C.: Resource usage protocols for iterators, http:\/\/www.cs.ru.nl\/~chaack\/papers\/iterators.pdf"},{"key":"16_CR16","unstructured":"Haack, C., Hurlin, C.: Separation logic contracts for a Java-like language with fork\/join. Technical Report 6430, INRIA (2008)"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Igarashi, A., Pierce, B., Wadler, P.: Featherweight Java: a minimal core calculus for Java and GJ. ACM Trans. Program. Lang. Syst.\u00a023(3) (2001)","DOI":"10.1145\/503502.503505"},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S., O\u2019Hearn, P.: BI as an assertion language for mutable data structures. In: Principles of Programming Languages (2001)","DOI":"10.1145\/360204.375719"},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"Krishnaswami, G.: Reasoning about iterators with separation logic. In: Specification and Verification of Component-Based Systems (2006)","DOI":"10.1145\/1181195.1181213"},{"key":"16_CR20","doi-asserted-by":"crossref","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java. SIGSOFT Software Engineering Notes\u00a031(3) (2006)","DOI":"10.1145\/1127878.1127884"},{"key":"16_CR21","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M.: Data groups: Specifying the modification of extended state. In: ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (1998)","DOI":"10.1145\/286936.286953"},{"key":"16_CR22","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.: Resources, concurrency and local reasoning. Theor. Comp. Science\u00a0375(1\u20133) (2007)","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"16_CR23","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W., Pym, D.J.: The logic of bunched implications. Bulletin of Symbolic Logic\u00a05(2) (1999)","DOI":"10.2307\/421090"},{"key":"16_CR24","volume-title":"Principles of Programming Languages","author":"P.W. O\u2019Hearn","year":"2004","unstructured":"O\u2019Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: Principles of Programming Languages, Venice, Italy. ACM Press, New York (2004)"},{"key":"16_CR25","unstructured":"Parkinson, M.: Local reasoning for Java. Technical Report UCAM-CL-TR-654, University of Cambridge (2005)"},{"key":"16_CR26","doi-asserted-by":"crossref","unstructured":"Parkinson, M., Bierman, G.: Separation logic and abstraction. In: Principles of Programming Languages (2005)","DOI":"10.1145\/1040305.1040326"},{"key":"16_CR27","doi-asserted-by":"crossref","unstructured":"Parkinson, M., Bierman, G.: Separation logic, abstraction and inheritance. In: Principles of Programming Languages (2008)","DOI":"10.1145\/1328438.1328451"},{"key":"16_CR28","volume-title":"Logic in Computer Science","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Logic in Computer Science, Copenhagen, Denmark. IEEE Press, Los Alamitos (2002)"},{"key":"16_CR29","series-title":"Lecture Notes in Computer Science","volume-title":"Programming Languages and Systems","author":"F. Smith","year":"2000","unstructured":"Smith, F., Walker, D., Morrisett, G.: Alias types. In: Smolka, G. (ed.) ESOP 2000 and ETAPS 2000. LNCS, vol.\u00a01782. Springer, Heidelberg (2000)"},{"key":"16_CR30","doi-asserted-by":"crossref","unstructured":"Wadler, P.: A taste of linear logic. In: Mathematical Foundations of Computer Science (1993)","DOI":"10.1007\/3-540-57182-5_12"}],"container-title":["Lecture Notes in Computer Science","Algebraic Methodology and Software Technology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-79980-1_16.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:35:21Z","timestamp":1619523321000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-79980-1_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540799795","9783540799801"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-79980-1_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}