{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,4,6]],"date-time":"2023-04-06T21:33:51Z","timestamp":1680816831674},"reference-count":14,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2014,3,20]],"date-time":"2014-03-20T00:00:00Z","timestamp":1395273600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2015,11]]},"DOI":"10.1007\/s10009-014-0310-9","type":"journal-article","created":{"date-parts":[[2014,3,19]],"date-time":"2014-03-19T22:40:54Z","timestamp":1395268854000},"page":"659-676","source":"Crossref","is-referenced-by-count":6,"title":["Solving the VerifyThis 2012 challenges with VeriFast"],"prefix":"10.1007","volume":"17","author":[{"given":"Bart","family":"Jacobs","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan","family":"Smans","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frank","family":"Piessens","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,3,20]]},"reference":[{"key":"310_CR1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions. Springer, Berlin (2004)"},{"key":"310_CR2","doi-asserted-by":"crossref","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P., Parkinson, M.: Permission accounting in separation logic. POPL (2005)","DOI":"10.1145\/1040305.1040327"},{"key":"310_CR3","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient smt solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS. In: Lecture Notes in Computer Science, vol. 4963, pp. 337\u2013340. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"310_CR4","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A., Stump, A.: The 2nd verified software competition: experience report. In: Klebanov, V., Grebing, S. (eds.), COMPARE2012: 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems. Manchester, UK, June 2012. EasyChair (2012)"},{"key":"310_CR5","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. CACM 12(10) (1969)","DOI":"10.1145\/363235.363259"},{"key":"310_CR6","unstructured":"Huisman, M., Klebanov, V., Monahan, R.: The VerifyThis 2012 website. http:\/\/fm2012.verifythis.org\/ (2012)"},{"key":"310_CR7","unstructured":"Jacobs, B., Smans, J., Piessens, F.: The VeriFast website. http:\/\/distrinet.cs.kuleuven.be\/software\/VeriFast\/ (2013)"},{"key":"310_CR8","doi-asserted-by":"crossref","unstructured":"Klebanov, V., M\u00fcller, P., Shankar, N., Leavens, G.T., W\u00fcstholz, V., Alkassar, E., Arthan, R., Bronish, D., Chapman, R., Cohen, E., Hillebrand, M., Jacobs, B., Rustan, K., Leino, M., Monahan, R., Piessens, F., Polikarpova, N., Ridge, T., Smans, J., Tobies, S., Tuerk, T., Ulbrich, M., Wei\u00df, B.: The 1st Verified Software Competition: Experience report. In: Butler, M., Schulte W. (eds) Proceedings, 17th International Symposium on Formal Methods (FM), vol. 6664 of LNCS. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-21437-0_14"},{"key":"310_CR9","first-page":"254","volume-title":"Software Safety and Security","author":"Tobias Nipkow","year":"2012","unstructured":"Nipkow, Tobias: Interactive proof: Introduction to Isabelle\/HOL. In: Grumberg, O., Nipkow, T., Hauptmann, B. (eds.) Software Safety and Security, pp. 254\u2013285. IOS Press, Amsterdam (2012)"},{"key":"310_CR10","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. CSL (2001)","DOI":"10.1007\/3-540-44802-0_1"},{"key":"310_CR11","doi-asserted-by":"crossref","unstructured":"Parkinson, M., Bierman, G.: Separation logic and abstraction. POPL (2005)","DOI":"10.1145\/1040305.1040326"},{"key":"310_CR12","doi-asserted-by":"crossref","unstructured":"Philippaerts, P., M\u00fchlberg, J.T., Penninckx, W., Smans, J., Jacobs, B., Piessens, F.: Software verification with VeriFast: industrial case studies. Sci. Comput. Progr (2013)","DOI":"10.1016\/j.scico.2013.01.006"},{"key":"310_CR13","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. LICS (2002)"},{"key":"310_CR14","unstructured":"Tuerk, T.: Local reasoning about while-loops. In: VSTTE Theory Workshop (2010)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0310-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-014-0310-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0310-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,8]],"date-time":"2019-08-08T13:28:27Z","timestamp":1565270907000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-014-0310-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,3,20]]},"references-count":14,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2015,11]]}},"alternative-id":["310"],"URL":"https:\/\/doi.org\/10.1007\/s10009-014-0310-9","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,3,20]]}}}