{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T08:10:09Z","timestamp":1748765409317,"version":"3.41.0"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319296128"},{"type":"electronic","value":"9783319296135"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-29613-5_8","type":"book-chapter","created":{"date-parts":[[2016,1,28]],"date-time":"2016-01-28T07:47:34Z","timestamp":1453967254000},"page":"124-141","source":"Crossref","is-referenced-by-count":4,"title":["Dynamic Frames Based Verification Method for Concurrent Java Programs"],"prefix":"10.1007","author":[{"given":"Wojciech","family":"Mostowski","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/3-540-44898-5_4","volume-title":"Static Analysis","author":"J Boyland","year":"2003","unstructured":"Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 55\u201372. Springer, Heidelberg (2003)"},{"doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: 17th IEEE Symposium on Logic in Computer Science, pp. 55\u201374. IEEE Computer Society (2002)","key":"8_CR2","DOI":"10.1109\/LICS.2002.1029817"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-642-03829-7_7","volume-title":"Foundations of Security Analysis and Design","author":"KRM Leino","year":"2009","unstructured":"Leino, K.R.M., M\u00fcller, P., Smans, J.: Verification of concurrent programs with Chalice. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007\/2008\/2009. LNCS, vol. 5705, pp. 195\u2013222. Springer, Heidelberg (2009)"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1007\/978-3-642-19718-5_23","volume-title":"Programming Languages and Systems","author":"MJ Parkinson","year":"2011","unstructured":"Parkinson, M.J., Summers, A.J.: The relationship between separation logic and implicit dynamic frames. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 439\u2013458. Springer, Heidelberg (2011)"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-319-07317-0_5","volume-title":"Formal Methods for Executable Software Models","author":"A Amighi","year":"2014","unstructured":"Amighi, A., Blom, S., Darabi, S., Huisman, M., Mostowski, W., Zaharieva-Stojanovski, M.: Verification of concurrent systems with VerCors. In: Bernardo, M., Damiani, F., H\u00e4hnle, R., Johnsen, E.B., Schaefer, I. (eds.) SFM 2014. LNCS, vol. 8483, pp. 172\u2013216. Springer, Heidelberg (2014)"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/11813040_19","volume-title":"FM 2006: Formal Methods","author":"IT Kassios","year":"2006","unstructured":"Kassios, I.T.: Dynamic frames: support for framing, dependencies and sharing without restrictions. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 268\u2013283. Springer, Heidelberg (2006)"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1007\/978-3-642-18070-5_10","volume-title":"Formal Verification of Object-Oriented Software","author":"PH Schmitt","year":"2011","unstructured":"Schmitt, P.H., Ulbrich, M., Wei\u00df, B.: Dynamic frames in Java dynamic logic. In: Beckert, B., March\u00e9, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 138\u2013152. Springer, Heidelberg (2011)"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1007\/978-3-319-12154-3_4","volume-title":"Verified Software: Theories, Tools and Experiments","author":"W Ahrendt","year":"2014","unstructured":"Ahrendt, W., Beckert, B., Bruns, D., Bubel, R., Gladisch, C., Grebing, S., H\u00e4hnle, R., Hentschel, M., Herda, M., Klebanov, V., Mostowski, W., Scheben, C., Schmitt, P.H., Ulbrich, M.: The KeY platform for verification and analysis of Java programs. In: Giannakopoulou, D., Kroening, D. (eds.) VSTTE 2014. LNCS, vol. 8471, pp. 55\u201371. Springer, Heidelberg (2014)"},{"issue":"3","key":"8_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1127878.1127884","volume":"31","author":"GT Leavens","year":"2006","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java. SIGSOFT 31(3), 1\u201338 (2006)","journal-title":"SIGSOFT"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-319-06410-9_9","volume-title":"FM 2014: Formal Methods","author":"S Blom","year":"2014","unstructured":"Blom, S., Huisman, M.: The VerCors tool for verification of concurrent programs. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 127\u2013131. Springer, Heidelberg (2014)"},{"doi-asserted-by":"crossref","unstructured":"Huisman, M., Mostowski, W.: A symbolic approach to permission accounting for concurrent reasoning. In: 14th International Symposium on Parallel and Distributed Computing (ISPDC 2015), pp. 165\u2013174. IEEE Computer Society (2015)","key":"8_CR11","DOI":"10.1109\/ISPDC.2015.26"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-642-38592-6_3","volume-title":"Formal Techniques for Distributed Systems","author":"W Mostowski","year":"2013","unstructured":"Mostowski, W.: A case study in formal verification using multiple explicit heaps. In: Beyer, D., Boreale, M. (eds.) FMOODS\/FORTE 2013. LNCS, vol. 7892, pp. 20\u201334. Springer, Heidelberg (2013)"},{"doi-asserted-by":"crossref","unstructured":"Mostowski, W., Ulbrich, M.: Dynamic dispatch for method contracts through abstract predicates. In: 15th International Conference on MODULARITY, pp. 109\u2013116. ACM (2015)","key":"8_CR13","DOI":"10.1145\/2724525.2724574"},{"doi-asserted-by":"crossref","unstructured":"Beckert, B., Schmitt, P.H.: Program verification using change information. In: Proceedings, Software Engineering and Formal Methods (SEFM) 2003, pp. 91\u201399. IEEE Press (2003)","key":"8_CR14","DOI":"10.1109\/SEFM.2003.1236211"},{"issue":"6","key":"8_CR15","doi-asserted-by":"publisher","first-page":"729","DOI":"10.1007\/s10009-013-0293-y","volume":"17","author":"D Bruns","year":"2013","unstructured":"Bruns, D., Mostowski, W., Ulbrich, M.: Implementation-level verification of algorithms with KeY. Softw. Tools Technol. Transf. 17(6), 729\u2013744 (2013)","journal-title":"Softw. Tools Technol. Transf."},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-319-22969-0_6","volume-title":"Software Engineering and Formal Methods","author":"S Blom","year":"2015","unstructured":"Blom, S., Huisman, M., Zaharieva-Stojanovski, M.: History-based verification of functional behaviour of concurrent programs. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 84\u201398. Springer, Heidelberg (2015)"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010)"},{"doi-asserted-by":"crossref","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: Palsberg, J., Abadi, M. (eds.) Principles of Programming Languages, pp. 259\u2013270. ACM (2005)","key":"8_CR18","DOI":"10.1145\/1047659.1040327"},{"key":"8_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-11(1:2)2015","volume":"11","author":"A Amighi","year":"2015","unstructured":"Amighi, A., Haack, C., Huisman, M., Hurlin, C.: Permission-based separation logic for multithreaded Java programs. Logical Methods Comput. Sci. 11, 1\u201366 (2015)","journal-title":"Logical Methods Comput. Sci."},{"issue":"1\u20133","key":"8_CR20","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","volume":"375","author":"PW O\u2019Hearn","year":"2007","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency and local reasoning. Theor. Comput. Sci. 375(1\u20133), 271\u2013307 (2007)","journal-title":"Theor. Comput. Sci."},{"doi-asserted-by":"crossref","unstructured":"Blom, S., Huisman, M., Kiniry, J.: How do developers use APIs? A case study in concurrency. In: International Conference on Engineering of Complex Computer Systems, pp. 212\u2013221. IEEE Computer Society (2013)","key":"8_CR21","DOI":"10.1109\/ICECCS.2013.39"},{"doi-asserted-by":"crossref","unstructured":"Amighi, A., Blom, S., Huisman, M., Mostowski, W., Zaharieva-Stojanovski, M.: Formal specifications for Java\u2019s synchronisation classes. In: Lafuente, A.L., Tuosto, E. (eds.) 22nd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, pp. 725\u2013733. IEEE Computer Society (2014)","key":"8_CR22","DOI":"10.1109\/PDP.2014.31"},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-540-79980-1_16","volume-title":"Algebraic Methodology and Software Technology","author":"C Haack","year":"2008","unstructured":"Haack, C., Hurlin, C.: Separation logic contracts for a Java-like language with fork\/join. In: Meseguer, J., Ro\u015fu, G. (eds.) AMAST 2008. LNCS, vol. 5140, pp. 199\u2013215. Springer, Heidelberg (2008)"},{"doi-asserted-by":"crossref","unstructured":"Boyland, J., M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Constraint semantics for abstract read permissions. In: Formal Techniques for Java-Like Programs (FTfJP). ACM (2014)","key":"8_CR24","DOI":"10.1145\/2635631.2635847"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-20398-5_4","volume-title":"NASA Formal Methods","author":"B Jacobs","year":"2011","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41\u201355. Springer, Heidelberg (2011)"},{"unstructured":"Juhasz, U., Kassios, I.T., M\u00fcller, P., Novacek, M., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. Technical report, ETH Z\u00fcrich (2014)","key":"8_CR26"},{"doi-asserted-by":"crossref","unstructured":"Bao, Y., Leavens, G.T., Ernst, G.: Translating separation logic into dynamic frames using fine-grained region logic. Technical report CS-TR-13-02a, Computer Science, University of Central Florida, March 2014","key":"8_CR27","DOI":"10.1145\/2786536.2786537"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, and Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-29613-5_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T07:33:17Z","timestamp":1748763197000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-29613-5_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319296128","9783319296135"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-29613-5_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}