{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T04:37:55Z","timestamp":1725856675477},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319336923"},{"type":"electronic","value":"9783319336930"}],"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-33693-0_29","type":"book-chapter","created":{"date-parts":[[2016,5,24]],"date-time":"2016-05-24T01:35:47Z","timestamp":1464053747000},"page":"457-473","source":"Crossref","is-referenced-by-count":0,"title":["Verifying Pointer Programs Using Separation Logic and Invariant Based Programming in Isabelle"],"prefix":"10.1007","author":[{"given":"Viorel","family":"Preoteasa","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,5,24]]},"reference":[{"key":"29_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/11757375","volume-title":"Petri Nets and Other Models of Concurrency - ICATPN 2006","author":"RJ Back","year":"2006","unstructured":"Back, R.J.: Invariant based programming. In: Donatelli, S., Thiagarajan, P.S. (eds.) ICATPN 2006. LNCS, vol. 4024, pp. 1\u201318. Springer, Heidelberg (2006)"},{"key":"29_CR2","doi-asserted-by":"crossref","unstructured":"Back, R.J., Preoteasa, V.: Semantics, proof rules of invariant based programs. In: 26th Symposium On Applied Computing - Software Verification and Testing Track. ACM (2011)","DOI":"10.1145\/1982185.1982532"},{"issue":"2","key":"29_CR3","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/s10817-013-9284-7","volume":"52","author":"C Ballarin","year":"2014","unstructured":"Ballarin, C.: Locales: a module system for mathematical theories. J. Autom. Reasoning 52(2), 123\u2013153 (2014)","journal-title":"J. Autom. Reasoning"},{"key":"29_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1007\/11804192_6","volume-title":"Formal Methods for Components and Objects","author":"J Berdine","year":"2006","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Smallfoot: modular automatic assertion checking with separation logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 115\u2013137. Springer, Heidelberg (2006)"},{"key":"29_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/978-3-642-34281-3_14","volume-title":"Formal Methods and Software Engineering","author":"F Bobot","year":"2012","unstructured":"Bobot, F., Filli\u00e2tre, J.-C.: Separation predicates: a taste of separation logic in first-order logic. In: Aoki, T., Taguchi, K. (eds.) ICFEM 2012. LNCS, vol. 7635, pp. 167\u2013181. Springer, Heidelberg (2012)"},{"key":"29_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/978-3-642-54108-7_10","volume-title":"Verified Software: Theories, Tools, Experiments","author":"F Bobot","year":"2014","unstructured":"Bobot, F., Filli\u00e2tre, J.-C., March\u00e9, C., Melquiond, G., Paskevich, A.: Preserving user proofs across specification changes. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 191\u2013201. Springer, Heidelberg (2014)"},{"key":"29_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/978-3-540-71067-7_14","volume-title":"Theorem Proving in Higher Order Logics","author":"L Bulwahn","year":"2008","unstructured":"Bulwahn, L., Krauss, A., Haftmann, F., Erk\u00f6k, L., Matthews, J.: Imperative functional programming with Isabelle\/HOL. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 134\u2013149. Springer, Heidelberg (2008)"},{"key":"29_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J-C Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3 \u2014 Where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013)"},{"key":"29_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/978-3-642-12251-4_9","volume-title":"Functional and Logic Programming","author":"F Haftmann","year":"2010","unstructured":"Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol. 6009, pp. 103\u2013117. Springer, Heidelberg (2010)"},{"key":"29_CR10","doi-asserted-by":"crossref","unstructured":"Heinen, J., Noll, T., Rieger, S.: Juggrnaut: Graph grammar abstraction for unbounded heap structures. In: Electronic Notes in Theoretical Computer Science, vol. 266, pp. 93\u2013107 (2010)","DOI":"10.1016\/j.entcs.2011.07.001"},{"key":"29_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"304","DOI":"10.1007\/978-3-642-17164-2_21","volume-title":"Programming Languages and Systems","author":"B Jacobs","year":"2010","unstructured":"Jacobs, B., Smans, J., Piessens, F.: A quick tour of the verifast program verifier. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 304\u2013311. Springer, Heidelberg (2010)"},{"key":"29_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"332","DOI":"10.1007\/978-3-642-32347-8_22","volume-title":"Interactive Theorem Proving","author":"G Klein","year":"2012","unstructured":"Klein, G., Kolanski, R., Boyton, A.: Mechanised separation algebra. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 332\u2013337. Springer, Heidelberg (2012)"},{"key":"29_CR13","doi-asserted-by":"crossref","unstructured":"Klein, G., Kolanski, R., Boyton, A.: Separation algebra. Archive of Formal Proofs, May 2012. http:\/\/afp.sf.net\/entries\/Separation_Algebra.shtml . Formal proof development","DOI":"10.1007\/978-3-642-32347-8_22"},{"key":"29_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1007\/978-3-319-22102-1_17","volume-title":"Interactive Theorem Proving","author":"P Lammich","year":"2015","unstructured":"Lammich, P.: Refinement to imperative\/HOL. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 253\u2013269. Springer, Heidelberg (2015)"},{"key":"29_CR15","unstructured":"Lammich, P., Meis, R.: A separation logic framework for imperative HOL. Archive of Formal Proofs, Nov 2012. http:\/\/afp.sf.net\/entries\/Separation_Logic_Imperative_HOL.shtml"},{"key":"29_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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: Voronkov, A., Clarke, E.M. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010)"},{"issue":"2","key":"29_CR17","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1016\/0020-0190(73)90012-4","volume":"2","author":"G Lindstrom","year":"1973","unstructured":"Lindstrom, G.: Scanning list structures without stacks or tag bits. Inform. Process. Lett. 2(2), 47\u201351 (1973)","journal-title":"Inform. Process. Lett."},{"key":"29_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/11823230_17","volume-title":"Static Analysis","author":"A Loginov","year":"2006","unstructured":"Loginov, A., Reps, T., Sagiv, M.: Automated verification of the deutsch-schorr-waite tree-traversal algorithm. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 261\u2013279. Springer, Heidelberg (2006)"},{"key":"29_CR19","doi-asserted-by":"crossref","first-page":"865","DOI":"10.1017\/S0956796808006953","volume":"18","author":"A Nanevski","year":"2008","unstructured":"Nanevski, A., Morrisett, G., Birkedal, L.: Hoare type theory, polymorphism and separation. J. Funct. Program. 18, 865\u2013911 (2008)","journal-title":"J. Funct. Program."},{"key":"29_CR20","doi-asserted-by":"crossref","unstructured":"Nanevski, A., Vafeiadis, V., Berdine, J.: Structuring the verification of heap-manipulating programs. In: Proceedings of POPL 2010, pp. 261\u2013274. ACM, New York (2010)","DOI":"10.1145\/1706299.1706331"},{"key":"29_CR21","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle\/HOL","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M. (eds.): Isabelle\/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)"},{"key":"29_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"Computer Science Logic","author":"PW O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 1\u201319. Springer, Heidelberg (2001)"},{"key":"29_CR23","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1016\/j.jlap.2013.09.001","volume":"84","author":"V Preoteasa","year":"2015","unstructured":"Preoteasa, V., Back, R.-J., Eriksson, J.: Verification and code generation for invariant diagrams in Isabelle. J. Logical Algebraic Methods Program. 84, 37\u201353 (2015)","journal-title":"J. Logical Algebraic Methods Program."},{"key":"29_CR24","doi-asserted-by":"crossref","unstructured":"Reynolds, J.: Separation logic: A logic for shared mutable data structures. In: 17th Annual IEEE Symposium on Logic in Computer Science. IEEE, July 2002","DOI":"10.1109\/LICS.2002.1029817"},{"key":"29_CR25","unstructured":"Thiemann, R.: Mutually recursive partial functions. Archive of Formal Proofs, Feb 2014. http:\/\/afp.sf.net\/entries\/Partial_Function_MR.shtml , Formal proof development"},{"key":"29_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/3-540-48256-3_12","volume-title":"Theorem Proving in Higher Order Logics","author":"M Wenzel","year":"1999","unstructured":"Wenzel, M.: Isar - a generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 167\u2013183. Springer, Heidelberg (1999)"},{"key":"29_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"402","DOI":"10.1007\/3-540-45931-6_28","volume-title":"Foundations of Software Science and Computation Structures","author":"H Yang","year":"2002","unstructured":"Yang, H., O\u2019Hearn, P.W.: A semantic basis for local reasoning. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 402\u2013416. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-33693-0_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,8]],"date-time":"2019-09-08T14:33:28Z","timestamp":1567953208000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-33693-0_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319336923","9783319336930"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-33693-0_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}