{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T10:38:30Z","timestamp":1648636710020},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2014,2,9]],"date-time":"2014-02-09T00:00:00Z","timestamp":1391904000000},"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-0300-y","type":"journal-article","created":{"date-parts":[[2014,2,8]],"date-time":"2014-02-08T10:51:16Z","timestamp":1391856676000},"page":"745-755","source":"Crossref","is-referenced-by-count":4,"title":["AutoProof\u00a0meets some verification challenges"],"prefix":"10.1007","volume":"17","author":[{"given":"Julian","family":"Tschannen","sequence":"first","affiliation":[]},{"given":"Carlo A.","family":"Furia","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Nordio","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,2,9]]},"reference":[{"issue":"6","key":"300_CR1","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1145\/1953122.1953145","volume":"54","author":"M Barnett","year":"2011","unstructured":"Barnett, M., F\u00e4hndrich, M., Leino, K.R.M., M\u00fcller, P., Schulte, W., Venter, H.: Specification and verification: the spec# experience. Commun. ACM 54(6), 81\u201391 (2011)","journal-title":"Commun. ACM"},{"key":"300_CR2","doi-asserted-by":"crossref","unstructured":"Barnett, M., Naumann, D.A.: Friends need a bit more: maintaining invariants over shared state. In: Kozen, D. (ed.) MPC, vol. 3125 of LNCS, pp. 54\u201384. Springer, Berlin, Heidelberg (2004)","DOI":"10.1007\/978-3-540-27764-4_5"},{"key":"300_CR3","unstructured":"Bobot, F., Filli\u00e2tre, J.-C., March\u00e9, C., Paskevich, A.: Why3: shepherd your herd of provers. In: Proceedings of the First International Workshop on Intermediate Verification Languages (Boogie\u201911), Wroclaw, Poland, pp. 53\u201364. (2011). http:\/\/research.microsoft.com\/en-us\/um\/people\/moskal\/boogie2011\/boogie_2011_all.pdf"},{"key":"300_CR4","unstructured":"Bormer, T., et al.: The COST IC0701 verification competition. In: Beckert, B., Damiani, F., Gurov, D. (eds.) FoVeOos, LNCS, pp. 3\u201321. Springer-Verlag, Berlin, Heidelberg (2012)"},{"key":"300_CR5","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A., Stump, A.: The 2nd verified software competition: experience report. In: Vladimir, K., Bernhard, B., Armin, B., Geoff, S. (eds.) Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems. pp. 36\u201349 (2012)"},{"key":"300_CR6","doi-asserted-by":"crossref","unstructured":"Gries, D.: The Science of Programming. Springer-Verlag, Berlin (1981)","DOI":"10.1007\/978-1-4612-5983-1"},{"key":"300_CR7","unstructured":"Huisman, M., Klebanov, V., Monahan, R.: VerifyThis verification competition. http:\/\/verifythis2012.cost-ic0701.org (2012)"},{"key":"300_CR8","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Smans, J., Piessens, F.: A quick tour of the VeriFast program verifier. In: Proceedings of APLAS 2010, pp. 304\u2013311. Springer (2010)","DOI":"10.1007\/978-3-642-17164-2_21"},{"key":"300_CR9","doi-asserted-by":"crossref","unstructured":"Klebanov, T. et al.: The 1st verified software competition: Experience report. In: Butler, M., Schulte, W. (eds.) FM, vol. 6664 of LNCS, pp. 154\u2013168. Springer, Berlin, Heidelberg (2011)","DOI":"10.1007\/978-3-642-21437-0_14"},{"key":"300_CR10","unstructured":"Leino, K.R.M.: This is Boogie 2. Technical report, Microsoft Research (2008)"},{"key":"300_CR11","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16, pp. 348\u2013370. Springer-Verlag, Berlin, Heidelberg (2010)","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"300_CR12","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., Monahan, R.: Reasoning about comprehensions with first-order SMT solvers. In Shin, S.Y., Ossowski, S. (eds.) Proceedings of the 2009 ACM symposium on applied computing (SAC\u201909), pp. 615\u2013622. ACM Press (2009)","DOI":"10.1145\/1529282.1529411"},{"key":"300_CR13","doi-asserted-by":"crossref","unstructured":"Naumann, D.A.: Observational purity and encapsulation. In: Cerioli, M (ed.) FASE, vol. 3442 of LNCS, pp. 190\u2013204. Springer, Berlin, Heidelberg (2005)","DOI":"10.1007\/978-3-540-31984-9_15"},{"key":"300_CR14","doi-asserted-by":"crossref","unstructured":"Nordio, M., Calcagno, C., Meyer, B., M\u00fcller, P., Tschannen, J.: Reasoning about function objects. In: Proceedings of TOOLS-EUROPE, vol. 6141 of LNCS, pp. 79\u201396. Springer (2010)","DOI":"10.1007\/978-3-642-13953-6_5"},{"key":"300_CR15","doi-asserted-by":"crossref","unstructured":"Nordio, M., Calcagno, C., M\u00fcller, P., Meyer, B..: A sound and complete program logic for Eiffel. In: Meyer, B (ed.) TOOLS-EUROPE, vol. 33, pp. 195\u2013214 (2009)","DOI":"10.1007\/978-3-642-02571-6_12"},{"issue":"7","key":"300_CR16","doi-asserted-by":"crossref","first-page":"104","DOI":"10.1145\/2209249.2209271","volume":"55","author":"D Patterson","year":"2012","unstructured":"Patterson, D.: For better or worse, benchmarks shape a field: technical perspective. Commun. ACM 55(7), 104\u2013104 (2012)","journal-title":"Commun. ACM"},{"key":"300_CR17","doi-asserted-by":"crossref","unstructured":"Polikarpova, N., Furia, C.A., Meyer, B.: Specifying reusable components. In Proceedings of VSTTE\u201910, vol. 6217 of LNCS, pp. 127\u2013141. Springer (2010)","DOI":"10.1007\/978-3-642-15057-9_9"},{"key":"300_CR18","doi-asserted-by":"crossref","unstructured":"Polikarpova, N., Furia, C.A., Pei, Y., Wei, Y., Meyer, B.: What good are strong specifications? In: David, N., Betty. H.C.C., Klaus, P. (eds.) ICSE, pp. 257\u2013266. ACM (2013) IEEE Press Piscataway, NJ, USA","DOI":"10.1109\/ICSE.2013.6606572"},{"key":"300_CR19","doi-asserted-by":"crossref","unstructured":"Polikarpova, N., Tschannen, J., Furia, C.A., Meyer, B.: Flexible invariants through semantic collaboration. http:\/\/arxiv.org\/abs\/1311.6329 (November 2013)","DOI":"10.1007\/978-3-319-06410-9_35"},{"key":"300_CR20","doi-asserted-by":"crossref","unstructured":"Tschannen, J., Furia, C.A., Nordio, M., Meyer, B.: Usable verification of object-oriented programs by combining static and dynamic techniques. In: Gilles, B., Alberto, P., Gerardo, S. (eds.) SEFM, vol. 7041 of LNCS, pp. 382\u2013398. Springer-Verlag, Berlin, Heidelberg (2011)","DOI":"10.1007\/978-3-642-24690-6_26"},{"key":"300_CR21","unstructured":"Tschannen, J., Furia, C.A., Nordio, M., Meyer, B.: Verifying Eiffel programs with Boogie. In: BOOGIE workshop. http:\/\/arxiv.org\/abs\/1106.4700 (2011)"},{"key":"300_CR22","doi-asserted-by":"crossref","unstructured":"Tschannen, J., Furia, C.A., Nordio, M., Meyer, B.: Automatic verification of advanced object-oriented features: the AutoProof approach. In: Meyer, B., Nordio, M (eds.) Tools for Practical Software Verification, vol. 7682 of LNCS, pp. 134\u2013156. Springer, Berlin, Heidelberg (2012)","DOI":"10.1007\/978-3-642-35746-6_5"},{"key":"300_CR23","doi-asserted-by":"crossref","unstructured":"Tschannen, J., Furia, C.A., Nordio, M., Meyer, B.: Program checking with less hassle. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE, vol. 8164 of LNCS, pp. 149\u2013169. Springer, Berlin, Heidelberg (2014)","DOI":"10.1007\/978-3-642-54108-7_8"}],"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-0300-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-014-0300-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0300-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,26]],"date-time":"2022-03-26T03:31:48Z","timestamp":1648265508000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-014-0300-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,2,9]]},"references-count":23,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2015,11]]}},"alternative-id":["300"],"URL":"https:\/\/doi.org\/10.1007\/s10009-014-0300-y","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,2,9]]}}}