{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,10]],"date-time":"2026-01-10T00:23:19Z","timestamp":1768004599072,"version":"3.49.0"},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2014,4,16]],"date-time":"2014-04-16T00:00:00Z","timestamp":1397606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2015,11]]},"DOI":"10.1007\/s10009-014-0308-3","type":"journal-article","created":{"date-parts":[[2014,4,15]],"date-time":"2014-04-15T14:36:46Z","timestamp":1397572606000},"page":"677-694","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":47,"title":["KIV: overview and VerifyThis competition"],"prefix":"10.1007","volume":"17","author":[{"given":"Gidon","family":"Ernst","sequence":"first","affiliation":[]},{"given":"J\u00f6rg","family":"Pf\u00e4hler","sequence":"additional","affiliation":[]},{"given":"Gerhard","family":"Schellhorn","sequence":"additional","affiliation":[]},{"given":"Dominik","family":"Haneberg","sequence":"additional","affiliation":[]},{"given":"Wolfgang","family":"Reif","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,4,16]]},"reference":[{"key":"308_CR1","doi-asserted-by":"crossref","unstructured":"Aehlig, K., Haftmann, F., Nipkow, T.: A compiled implementation of normalization by evaluation. In: Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics (THOL 08), vol. 5170, pp. 39\u201354. Springer LNCS, Berlin (2008)","DOI":"10.1007\/978-3-540-71067-7_8"},{"issue":"1","key":"308_CR2","first-page":"91","volume":"23","author":"S B\u00e4umler","year":"2011","unstructured":"B\u00e4umler, S., Schellhorn, G., Tofan, B., Reif, W.: Proving linearizability with temporal logic. FAC J 23(1), 91\u2013112 (2011)","journal-title":"FAC J"},{"key":"308_CR3","doi-asserted-by":"crossref","unstructured":"B\u00f6rger, E., St\u00e4rk, R.F.: Abstract state machines\u2014a method for high-level system design and analysis. Springer, Berlin (2003)","DOI":"10.1007\/978-3-642-18216-7"},{"key":"308_CR4","doi-asserted-by":"crossref","unstructured":"Bormer, T., Brockschmidt, M., Distefano, D., Ernst, G., Filliatre, J. C., Grigore, R., Huisman, M., Klebanov, V., Marche, C., Monahan, R., Mostowski, W.I., Poiikarpova, N., Scheben, C., Schellhorn, G., Tofan, B., Tschannen, J., Ulbrich, M.: The cost ic0701 verification competition 2011. In: International Conference on Formal Verification of Object-Oriented Software, FoVeOOS 2011, vol. 7421, pp. 3\u201321. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-31762-0_2"},{"key":"308_CR5","first-page":"309","volume":"74","author":"RM Burstall","year":"1974","unstructured":"Burstall, R.M.: Program proving as hand simulation with a little induction. Inf. Process. 74, 309\u2013312 (1974)","journal-title":"Inf. Process."},{"key":"308_CR6","doi-asserted-by":"crossref","unstructured":"Derrick, J., Schellhorn, G., Wehrheim, H.: Mechanising a correctness proof for a lock-free concurrent stack. In: Proceedings of FMOODS 2008, Oslo, vol. 5051, pp. 78\u201395. Springer LNCS, Berlin (2008)","DOI":"10.1007\/978-3-540-68863-1_6"},{"key":"308_CR7","doi-asserted-by":"crossref","unstructured":"Ernst, G., Schellhorn, G., Haneberg, D., Pf\u00e4hler, J., Reif, W.: Verification of a virtual filesystem switch. In: Proceedings of Verified Software: Theories, Tools, Experiments, vol. 8164, pp. 242\u2013261. Springer, Berlin (2014)","DOI":"10.1007\/978-3-642-54108-7_13"},{"key":"308_CR8","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Schwartz, J.T. (ed.) Proceedings of the Symposium on Applied Mathematics, vol. 19, pp. 19\u201332. American Mathematical Society, New York (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"308_CR9","doi-asserted-by":"crossref","unstructured":"Fuch\u00df, T., Reif, W., Schellhorn, G., Stenzel, K.: Three Selected Case Studies in Verification. In: Broy, M., J\u00e4hnichen, S.: (eds.) KORSO: Methods, Languages, and Tools for the Construction of Correct Software\u2014Final Report, vol. 1009. Springer LNCS, Berlin (1995)","DOI":"10.1007\/BFb0015472"},{"key":"308_CR10","doi-asserted-by":"crossref","unstructured":"Grandy, H., Bischof, M., Schellhorn, G., Reif, W., Stenzel, K.: Verification of Mondex Electronic Purses with KIV: From a Security Protocol to Verified Code. In: FM 2008: 15th International Symposium on Formal Methods, vol. 5014. Springer LNCS, Berlin (2008)","DOI":"10.1007\/978-3-540-68237-0_13"},{"key":"308_CR11","unstructured":"Gurevich, Y.: Evolving algebras 1993: Lipari guide. In: B\u00f6rger, E. (ed.) Specification and validation methods, pp. 9\u201336. Oxford Univ. Press, Oxford (1995)"},{"key":"308_CR12","unstructured":"Haneberg, D., B\u00e4umler, S., Balser, M., Grandy, H., Ortmeier, F., Reif, W., Schellhorn, G., Schmitt, J., Stenzel, K.: The user interface of the KIV verification system\u2014as system description. Electronic Notes in Theoretical Computer Science UITP special issue (2006)"},{"key":"308_CR13","unstructured":"Haneberg, D., Moebius, N., Reif, W., Schellhorn, G., Stenzel, K.: Mondex: engineering a provable secure electronic purse. Int. J. Softw. Inf. 5(1):159\u2013184 (2011). http:\/\/www.ijsi.org"},{"key":"308_CR14","doi-asserted-by":"crossref","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic logic. In: Gabbay, D., Guenther, F., (eds.) Handbook of philosophical logic, vol. 4, , 2nd edn, pp. 99\u2013217. Kluwer Academic Publishers, Dordecht (2002)","DOI":"10.1007\/978-94-017-0456-4_2"},{"key":"308_CR15","unstructured":"Huisman, M., Klebanov, V., Monahan, R.: On the organisation of program verification competitions. In: Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems (COMPARE), CEUR Workshop Proceedings, vol. 873 CEUR-WS.org (2012)"},{"key":"308_CR16","unstructured":"Jones, C.B.: Specification and design of (parallel) programs. In: Proceedings of IFIP\u201983, pp. 321\u2013332. North-Holland, Amsterdam (1983)"},{"key":"308_CR17","unstructured":"Web presentation of the KIV solutions for the VerifyThis Competition, 2012. http:\/\/www.informatik.uni-augsburg.de\/swt\/projects\/verifythis-competition-2012"},{"key":"308_CR18","unstructured":"Manber, U., Myers, G.: Suffix Arrays: a new method for on-Line string searches. In Proceedings of the first annual ACM-SIAM symposium on Discrete algorithms, SODA \u201990, pp. 319\u2013327. Society for Industrial and Applied Mathematics (1990)"},{"issue":"2","key":"308_CR19","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1145\/359340.359353","volume":"21","author":"Z Manna","year":"1978","unstructured":"Manna, Z., Waldinger, R.: Is \u201csometime\u201d sometimes better than \u201calways\u201d?: intermittent assertions in proving program correctness. Commun. ACM 21(2), 159\u2013172 (1978)","journal-title":"Commun. ACM"},{"issue":"2","key":"308_CR20","doi-asserted-by":"crossref","first-page":"10","DOI":"10.1109\/MC.1985.1662795","volume":"18","author":"B Moszkowski","year":"1985","unstructured":"Moszkowski, B.: A temporal logic for multilevel reasoning about hardware. IEEE Comput. 18(2), 10\u201319 (1985)","journal-title":"IEEE Comput."},{"key":"308_CR21","doi-asserted-by":"crossref","unstructured":"Owre, S., Rajan, S., Rushby, J.M., Shankar, N., Srivas, M.: PVS: Combining specification, proof checking, and model checking. In: Alur, R., Henzinger, T.A. (eds.) Computer Aided Verification (CAV), vol. 1102. Springer LNCS, Berlin (1996)","DOI":"10.1007\/3-540-61474-5_91"},{"key":"308_CR22","doi-asserted-by":"crossref","unstructured":"Pf\u00e4hler, J., Ernst, G., Schellhorn, G., Haneberg, D., Reif, W.: Formal specification of an erase block management layer for flash memory. In: Bertacco, V., Legay, A. (eds.) Hardware and software: verification and testing, vol. 8244, pp. 214\u2013229. Springer International Publishing LNCS, Berlin (2013)","DOI":"10.1007\/978-3-319-03077-7_15"},{"key":"308_CR23","doi-asserted-by":"crossref","unstructured":"Reif, W., Schellhorn, G., Stenzel, K., Balser, M.: Structured specifications and interactive proofs with KIV. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction\u2014A Basis for Applications, vol. II, pp. 13\u201339. Kluwer, Dordrecht (1998)","DOI":"10.1007\/978-94-017-0435-9_1"},{"key":"308_CR24","doi-asserted-by":"crossref","unstructured":"Reif, W., Schellhorn, G., Stenzel, K., Balser, M.: Structured specifications and interactive proofs with KIV. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction\u2014A Basis for Applications, vol. II Systems and Implementation Techniques. Interactive Theorem Proving, Chap. 1, pp. 13\u201339. Kluwer Academic Publishers, Dordrecht (1998)","DOI":"10.1007\/978-94-017-0435-9_1"},{"key":"308_CR25","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings of LICS, pp. 55\u201374. IEEE Computer Society, New York (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"issue":"1","key":"308_CR26","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1093\/logcom\/3.1.47","volume":"3","author":"P Robinson","year":"1993","unstructured":"Robinson, P., Staples, J.: Formalizing a hierarchical structure of practical mathematical reasoning. J. Logic Comput. 3(1), 47\u201361 (1993)","journal-title":"J. Logic Comput."},{"key":"308_CR27","doi-asserted-by":"crossref","unstructured":"Schellhorn, G., Ahrendt, W.: The WAM case study: verifying compiler correctness for prolog with KIV. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction\u2014A Basis for Applications, vol. III. Applications, Automated Theorem Proving in Software Engineering, Chap. 3, pp. 165\u2013194. Kluwer Academic Publishers, Dordecht (1998)","DOI":"10.1007\/978-94-017-0437-3_7"},{"key":"308_CR28","doi-asserted-by":"crossref","unstructured":"Schellhorn, G., Grandy, H., Haneberg, D., Moebius, N., Reif, W.: A systematic verification approach for Mondex electronic purses using ASMs. In: Gl\u00e4sser, U., Abrial, J.-R. (eds.) Dagstuhl Seminar on Rigorous Methods for Software Construction and Analysis, vol. 5115, pp. 93\u2013110. Springer LNCS, Berlin (2009)","DOI":"10.1007\/978-3-642-11447-2_7"},{"key":"308_CR29","doi-asserted-by":"crossref","unstructured":"Schellhorn, G., Tofan, B., Ernst, G., Reif, W.: Interleaved programs and rely-guarantee reasoning with ITL. In: Proceedings of the 18th International Symposium on Temporal Representation and Reasoning (TIME), pp. 99\u2013106. IEEE Computer Society Press, New York (2011)","DOI":"10.1109\/TIME.2011.12"},{"key":"308_CR30","doi-asserted-by":"crossref","unstructured":"Schierl, A., Schellhorn, G., Haneberg, D., Reif, W.: Abstract specification of the UBIFS file system for flash memory. In: Proceedings of FM 2009: Formal Methods, vol. 5850, pp. 190\u2013206. Springer LNCS, Berlin (2009)","DOI":"10.1007\/978-3-642-05089-3_13"},{"key":"308_CR31","unstructured":"Stenzel, K.: Verification of Java Card Programs. PhD thesis, Universit\u00e4t Augsburg, Fakult\u00e4t f\u00fcr Angewandte Informatik, http:\/\/www.opus-bayern.de\/uni-augsburg\/volltexte\/2005\/122\/ (2005)"},{"key":"308_CR32","unstructured":"Szabo, M.E. (ed.): The Collected Papers of Gerhard Gentzen. North-Holland, Amsterdam (1969)"},{"key":"308_CR33","doi-asserted-by":"crossref","unstructured":"Tofan, B., Schellhorn, G., Reif, W.: Formal verification of a lock-free stack with hazard pointers. In Proc. ICTAC, vol. 6916, pp. 239\u2013255. Springer LNCS, Berlin (2011)","DOI":"10.1007\/978-3-642-23283-1_16"},{"key":"308_CR34","unstructured":"Tofan, B., Schellhorn, G., Reif, W.: Local rely-guarantee conditions for linearizability and lock-freedom. Karlsruhe Reports in Informatics 2011\u201326, Karlsruhe Institute of Technology (2011)"},{"key":"308_CR35","unstructured":"Tuerk, T.: Local reasoning about while-loops. In: M\u00fcller, P., Naumann, D., Yang, H. (eds.) Proceedings, VS-Theory Workshop of VSTTE 2010, pp. 29\u201339 (2010)"},{"key":"308_CR36","unstructured":"The Alloy Project. http:\/\/alloy.mit.edu"},{"issue":"2","key":"308_CR37","first-page":"149","volume":"9","author":"Q Xu","year":"1997","unstructured":"Xu, Q., de Roever, W.-P., He, J.: The rely-guarantee method for verifying shared variable concurrent programs. FAC J 9(2), 149\u2013174 (1997)","journal-title":"FAC J"}],"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-0308-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-014-0308-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0308-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,9]],"date-time":"2019-08-09T14:58:47Z","timestamp":1565362727000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-014-0308-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,4,16]]},"references-count":37,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2015,11]]}},"alternative-id":["308"],"URL":"https:\/\/doi.org\/10.1007\/s10009-014-0308-3","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,4,16]]}}}