{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T01:22:28Z","timestamp":1743038548014,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540631040"},{"type":"electronic","value":"9783540691402"}],"license":[{"start":{"date-parts":[[1997,1,1]],"date-time":"1997-01-01T00:00:00Z","timestamp":852076800000},"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":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63104-6_10","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T18:03:36Z","timestamp":1330279416000},"page":"69-72","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Proving System Correctness with KIV 3.0"],"prefix":"10.1007","author":[{"given":"Wolfgang","family":"Reif","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gerhard","family":"Schellhorn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kurt","family":"Stenzel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"10_CR1","unstructured":"M. Abadi, M. Burrows, B. Lampson, and G. Plotkin, A Calculus for Access Control in Distributed Systems. In J. Feigenbaum, editor, CRYPTO '91. Springer LNAI 576, 1991."},{"key":"10_CR2","volume-title":"Logic Programming: Formal Methods and Practical Applications, volume 11 of Studies in Computer Science and Artificial Intelligence","author":"E. B\u00f6rger","year":"1995","unstructured":"Egon B\u00f6rger and Dean Rosenzweig. The WAM-definition and compiler correctness. In Christoph Beierle and Lutz Pl\u00fcmer, editors, Logic Programming: Formal Methods and Practical Applications, volume 11 of Studies in Computer Science and Artificial Intelligence. North-Holland, Amsterdam, 1995."},{"key":"10_CR3","unstructured":"M. Fr\u00f6hlich and M. Werner. Demonstration of the interactive graph visualization system daVinci. In R. Tamassia and I. Tollis, editors, DIMACS Workshop on Graph Drawing '94. Proceedings, Springer LNCS 894. Princeton (USA), 1994. http:\/\/www.informatik.uni-bremen.de\/~davinci\/."},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"T. Fuch\u00df, W. Reif, G. Schellhorn, and K. Stenzel. Three Selected Case Studies in Verification. In M. Broy and S. J\u00e4hnichen, editors, KORSO: Methods, Languages, and Tools for the Construction of Correct Software \u2014 Final Report. Springer LNCS 1009, 1995.","DOI":"10.1007\/BFb0015472"},{"key":"10_CR5","unstructured":"R. Goldblatt. Axiomatising the Logic of Computer Programming. Springer LNCS 130, 1982."},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"P. Graf. Term Indexing. Springer LNCS 1053, 1996.","DOI":"10.1007\/3-540-61040-5"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"S. Kaplan. A compiler for conditional term rewriting systems. In 2nd Conf. on Rewriting Techniques auf Applications. Proceedings. Bordeaux, France, Springer LNCS 256, 1987.","DOI":"10.1007\/3-540-17220-3_3"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"W. Reif. The KIV-approach to Software Verification. In M. Broy and S. J\u00e4hnichen, editors, KORSO: Methods, Languages, and Tools for the Construction of Correct Software \u2014 Final Report. Springer LNCS 1009, 1995.","DOI":"10.1007\/BFb0015471"},{"key":"10_CR9","volume-title":"Tenth Annual Conference on Computer Assurance","author":"W. Reif","year":"1995","unstructured":"W. Reif, G. Schellhorn, and K. Stenzel. Interactive Correctness Proofs for Software Modules Using KIV. In Tenth Annual Conference on Computer Assurance, IEEE press. NIST, Gaithersburg (MD), USA, 1995."},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"W. Reif and K. Stenzel. Reuse of Proofs in Software Verification. In R. Shyamasundar, editor, Foundation of Software Technology and Theoretical Computer Science. Proceedings, Springer LNCS 761. Bombay, India, 1993.","DOI":"10.1007\/3-540-57529-4_61"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"D. T. Sanella and M. Wirsing. A kernel language for algebraic specification and implementation. In Coll. on Foundations of Computation Theory, Springer LNCS 158. Link\u00f6ping, Sweden, 1983.","DOI":"10.1007\/3-540-12689-9_122"},{"key":"10_CR12","unstructured":"G. Schellhorn and W. Ahrendt. Reasoning about Abstract State Machines: The WAM Case Study. Journal of Universal Computer Science (JUCS), 1997. to appear."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-14"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63104-6_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T08:44:18Z","timestamp":1558255458000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63104-6_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540631040","9783540691402"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-63104-6_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]},"assertion":[{"value":"8 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}