{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,24]],"date-time":"2025-09-24T08:52:26Z","timestamp":1758703946473},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2013,11,17]],"date-time":"2013-11-17T00:00:00Z","timestamp":1384646400000},"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-013-0293-y","type":"journal-article","created":{"date-parts":[[2013,11,16]],"date-time":"2013-11-16T13:55:04Z","timestamp":1384610104000},"page":"729-744","source":"Crossref","is-referenced-by-count":8,"title":["Implementation-level verification of algorithms with KeY"],"prefix":"10.1007","volume":"17","author":[{"given":"Daniel","family":"Bruns","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wojciech","family":"Mostowski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mattias","family":"Ulbrich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2013,11,17]]},"reference":[{"key":"293_CR1","doi-asserted-by":"crossref","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: an overview. In: Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS), International Workshop, 2004, Revised Selected Papers. LNCS, vol. 3362, pp. 49\u201369. Springer (2005)","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"293_CR2","unstructured":"Beckert, B., Grebing, S.: Evaluating the usability of interactive verification systems. In: Klebanov, V., Beckert, B., Biere, A., Sutcliffe, G. (eds.) 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems (COMPARE) 2012, CEUR Workshop Proceedings, vol. 873 (2012)"},{"key":"293_CR3","doi-asserted-by":"crossref","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software: The KeY Approach. LNCS, vol. 4334. Springer (2007)","DOI":"10.1007\/978-3-540-69061-0"},{"key":"293_CR4","unstructured":"Blelloch, G.E.: Prefix sums and their applications. Tech. Rep. CMU-CS-90-190, School of Computer Science, Carnegie Mellon University (1990)"},{"key":"293_CR5","doi-asserted-by":"crossref","unstructured":"Bormer, T., Brockschmidt, M., Distefano, D., Ernst, G., Filli\u00e2tre, J.C., Grigore, R., Huisman, M., Klebanov, V., March\u00e9, C., Monahan, R., Mostowski, W., Polikarpova, N., Scheben, C., Schellhorn, G., Tofan, B., Tschannen, J., Ulbrich, M.: The COST IC0701 verification competition 2011. In: Beckert, B., Damiani, F., Gurov, D. (eds.) Revised Selected Papers, International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2011). LNCS, vol. 7421, pp. 3\u201321. Springer (2012)","DOI":"10.1007\/978-3-642-31762-0_2"},{"key":"293_CR6","doi-asserted-by":"crossref","unstructured":"Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. In: Arts, T., Fokkink, W. (eds.) Proceedings of the Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 03). ENTCS, vol. 80, pp. 73\u201389. Elsevier (2003)","DOI":"10.1016\/S1571-0661(04)80810-7"},{"issue":"6","key":"293_CR7","doi-asserted-by":"crossref","first-page":"583","DOI":"10.1002\/spe.649","volume":"35","author":"Y Cheon","year":"2005","unstructured":"Cheon, Y., Leavens, G.T., Sitaraman, M., Edwards, S.: Model variables: cleanly supporting abstraction in design by contract. Softw. Pract. Exp. 35(6), 583\u2013599 (2005)","journal-title":"Softw. Pract. Exp."},{"issue":"9","key":"293_CR8","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1145\/1995376.1995394","volume":"54","author":"L Moura De","year":"2011","unstructured":"De Moura, L., Bj\u00f8rner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69\u201377 (2011)","journal-title":"Commun. ACM"},{"key":"293_CR9","unstructured":"Filli\u00e2tre, J.C., March\u00e9, C.: The Why\/Krakatoa\/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) 19th International Conference on Computer Aided Verification. LNCS, vol. 4590. Springer (2007)"},{"key":"293_CR10","unstructured":"Filli\u00e2tre, J.C., Paskevich, A., Stump, A.: The 2nd verified software competition: experience report. In: Beckert, B., Biere, A., Klebanov, V., Sutcliffe, G. (eds.) 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems (COMPARE) 2012, CEUR Workshop Proceedings, vol. 873 (2012)"},{"key":"293_CR11","doi-asserted-by":"crossref","first-page":"497","DOI":"10.1007\/978-94-009-6259-0_10","volume-title":"Handbook of Philosophical Logic, Volume II: Extensions of Classical Logic","author":"D Harel","year":"1984","unstructured":"Harel, D.: Dynamic logic. In: Gabbay, D., Guenther, F. (eds.) Handbook of Philosophical Logic, Volume II: Extensions of Classical Logic, pp. 497\u2013604. D. Reidel Publishing Co., Dordrecht (1984)"},{"key":"293_CR12","doi-asserted-by":"crossref","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.G., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NASA Formal Methods\u2014Third International Symposium, 2011. LNCS, vol. 6617, pp. 41\u201355. Springer (2011)","DOI":"10.1007\/978-3-642-20398-5_4"},{"issue":"3","key":"293_CR13","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1007\/s00165-010-0152-5","volume":"23","author":"IT Kassios","year":"2011","unstructured":"Kassios, I.T.: The dynamic frames theory. Form. Asp. Comput. 23(3), 267\u2013288 (2011)","journal-title":"Form. Asp. Comput."},{"key":"293_CR14","doi-asserted-by":"crossref","unstructured":"Kassios, I.T., M\u00fcller, P., Schwerhoff, M.: Comparing verification condition generation with symbolic execution: an experience report. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) Verified Software Theories Tools Experiments (VSTTE) 2012. LNCS, vol. 7152, pp. 196\u2013208. Springer (2012)","DOI":"10.1007\/978-3-642-27705-4_16"},{"key":"293_CR15","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., Leino, K.R.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) 2011. LNCS, vol. 6664, pp. 154\u2013168. Springer (2011)","DOI":"10.1007\/978-3-642-21437-0_14"},{"issue":"3","key":"293_CR16","doi-asserted-by":"crossref","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":"293_CR17","doi-asserted-by":"crossref","unstructured":"Mostowski, W.: Formal reasoning about non-atomic Java Card methods in dynamic logic. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) Proceedings, Formal Methods (FM) 2006. LNCS, vol. 4085, pp. 444\u2013459. Springer (2006)","DOI":"10.1007\/11813040_30"},{"key":"293_CR18","unstructured":"Mostowski, W.: Fully verified Java Card API reference implementation. In: Beckert, B. (ed.) 4th International Verification Workshop, CEUR WS, vol. 259 (2007)"},{"key":"293_CR19","unstructured":"The on-line encyclopedia of integer sequences. http:\/\/oeis.org\/A006519\/ . Retrieved 30\/07\/2013"},{"key":"293_CR20","doi-asserted-by":"crossref","unstructured":"Parkinson, M., Bierman, G.: Separation logic and abstraction. SIGPLAN Notes 40(1), 247\u2013258 (2005)","DOI":"10.1145\/1047659.1040326"},{"key":"293_CR21","doi-asserted-by":"crossref","unstructured":"Scheben, C., Schmitt, P.H.: Verification of information flow properties of Java programs without approximations. In: Formal Verification of Object-Oriented Software. LNCS, vol. 7421, pp. 232\u2013249. Springer (2012)","DOI":"10.1007\/978-3-642-31762-0_15"},{"key":"293_CR22","doi-asserted-by":"crossref","unstructured":"Schmitt, P.H., Tonin, I.: Verifying the Mondex case study. In: Hinchey, M., Margaria, T. (eds.) Proceedings of the 5th IEEE International Conference on Software Engineeging and Formal Methods (SEFM), pp. 47\u201356. IEEE Press (2007)","DOI":"10.1109\/SEFM.2007.47"},{"key":"293_CR23","unstructured":"Schulte, W., Songtao, X., Smans, J., Piessens, F.: A glimpse of a verifying C compiler. In: C\/C++ Verification Workshop (2007). https:\/\/lirias.kuleuven.be\/handle\/123456789\/146853"},{"key":"293_CR24","unstructured":"Sedgewick, R., Wayne, K.: Algorithms, 4th edn. Addison-Wesley, Reading (2011)"},{"key":"293_CR25","doi-asserted-by":"crossref","unstructured":"Stenzel, K.: A formally verified calculus for full Java Card. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) Algebraic Methodology and Software Technology, 10th International Conference, AMAST 2004. LNCS, vol. 3116, pp. 491\u2013505. Springer (2004)","DOI":"10.1007\/978-3-540-27815-3_37"},{"key":"293_CR26","unstructured":"Wei\u00df, B.: Deductive verification of object-oriented software: dynamic frames, dynamic logic and predicate abstraction. Ph.D. thesis, Karlsruhe Institute of Technology (2011)"}],"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-013-0293-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-013-0293-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-013-0293-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,12]],"date-time":"2022-03-12T13:41:52Z","timestamp":1647092512000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-013-0293-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,11,17]]},"references-count":26,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2015,11]]}},"alternative-id":["293"],"URL":"https:\/\/doi.org\/10.1007\/s10009-013-0293-y","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,11,17]]}}}