{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:18:04Z","timestamp":1725488284757},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540664628"},{"type":"electronic","value":"9783540482574"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48257-1_23","type":"book-chapter","created":{"date-parts":[[2007,7,20]],"date-time":"2007-07-20T16:25:09Z","timestamp":1184948709000},"page":"330-337","source":"Crossref","is-referenced-by-count":11,"title":["KIV 3.0 for Provably Correct Systems"],"prefix":"10.1007","author":[{"given":"Michael","family":"Balser","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wolfgang","family":"Reif","sequence":"additional","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","reference":[{"key":"23_CR1","unstructured":"M. Abadi, M. Burrows, B. Lampson, and G. Plotkin. A Calculus for Access Control in Distributed Systems. In J. Feigenbaum, editor, CRYPTO\u2019 91. Springer LNAI 576, 1991."},{"key":"23_CR2","doi-asserted-by":"crossref","unstructured":"W. Ahrendt, B. Beckert, R. H\u00e4hnle, W. Menzel, W. Reif, G. Schellhorn, and P. Schmitt. Integrating of Automated and Interactive Theorem Proving. In W. Bibel and P. Schmitt, editors, Automated Deduction \u2014 A Basis for Applications, volume I: Foundations, chapter 3: Interactive Theorem Proving. Kluwer Academic Publishers, 1998.","DOI":"10.1007\/978-94-017-0435-9_4"},{"key":"23_CR3","series-title":"Studies in Computer Science and Artificial Intelligence","volume-title":"Logic Programming: Formal Methods and Practical Applications","author":"E. B\u00f6rger","year":"1995","unstructured":"E. B\u00f6rger and D. Rosenzweig. The WAM\u2014definition 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":"23_CR4","series-title":"Lect Notes Comput Sci","volume-title":"DIM ACS Workshop on Graph Drawing\u2019 94. Proceedings","author":"M. Fr\u00f6hlich","year":"1994","unstructured":"M. Fr\u00f6hlich and M. Werner. Demonstration of the interactive graph visualization system daVinci. In R. Tamassia and I. Tollis, editors, DIM ACS Workshop on Graph Drawing\u2019 94. Proceedings, Springer LNCS 894. Princeton (USA), 1994. \n                    http:\/\/www.informatik.uni-bremen.de\/~davinci\/\n                    \n                  ."},{"key":"23_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0015472","volume-title":"KORSO: Methods, Languages, and Tools for the Construction of Correct Software-Final Report","author":"T. Fuch\u00df","year":"1995","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-Final Report. Springer LNCS 1009, 1995."},{"key":"23_CR6","series-title":"Lect Notes Comput Sci","volume-title":"Axiomatising the Logic of Computer Programming","author":"R. Goldblatt","year":"1982","unstructured":"R. Goldblatt. Axiomatising the Logic of Computer Programming. Springer LNCS 130, 1982."},{"key":"23_CR7","doi-asserted-by":"crossref","unstructured":"M. Gordon. HOL: A Proof Generating System for Higher-order Logic. In G. Birtwistle and P.A. Subrahmanyam, editors, VLSI Specification and Synthesis. Kluwer Academic Publishers, 1988.","DOI":"10.1007\/978-1-4613-2007-4_3"},{"key":"23_CR8","series-title":"Lect Notes Comput Sci","volume-title":"Term Indexing","author":"P. Graf","year":"1996","unstructured":"P. Graf. Term Indexing. Springer LNCS 1053, 1996."},{"key":"23_CR9","unstructured":"M. Gurevich. Evolving algebras 1993: Lipari guide. In E. B\u00f6rger, editor, Specification and Validation Methods. Oxford University Press, 1995."},{"key":"23_CR10","series-title":"Lect Notes Comput Sci","volume-title":"Logical Foundations of Computer Science","author":"M. Heisel","year":"1989","unstructured":"M. Heisel, W. Reif, and W. Stephan. A Dynamic Logic for Program Verification. In A. Meyer and M. Taitslin, editors, Logical Foundations of Computer Science. Springer LNCS 363, 1989."},{"key":"23_CR11","unstructured":"D. Hutter, B. Langenstein, F. Koob, W. Reif, C. Sengler, W. Stephan, M. Ullmann, M. Wittmann, and A. Wolpers. The VSE Development Method \u2014 A Way to Engineer High-Assurance Software Systems. In Bredereke Gotzheim, editor, GI\/ITG Tagung Formale Beschreibungstechniken f\u00fcr verteilte Systeme. Universit\u00e4t Kaiserslautern, 1995."},{"key":"23_CR12","series-title":"Lect Notes Comput Sci","volume-title":"2nd Conf. on Rewriting Techniques anf Applications. Proceedings","author":"S. Kaplan","year":"1987","unstructured":"S. Kaplan. A compiler for conditional term rewriting systems. In 2nd Conf. on Rewriting Techniques anf Applications. Proceedings. Bordeaux, France, Springer LNCS 256, 1987."},{"key":"23_CR13","doi-asserted-by":"crossref","unstructured":"M. Kaufmann and J Moore. An industrial strength theorem prover for a logic based on common lisp. IEEE Transactions on Software Engineering, 23(4), April 1997.","DOI":"10.1109\/32.588534"},{"key":"23_CR14","doi-asserted-by":"crossref","unstructured":"S. Owre, J. M. Rushby, and N. Shankar. PVS: A Prototype Verification System. In D. Kapur, editor, Automated Deduction-CADE-11. Proceedings, Springer LNAI 607. Saratoga Springs, NY, USA, 1992.","DOI":"10.1007\/3-540-55602-8_217"},{"key":"23_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabella A Generic Theorem Prover","author":"L. C. Paulson","year":"1994","unstructured":"L. C. Paulson. Isabella A Generic Theorem Prover. Springer LNCS 828, 1994."},{"key":"23_CR16","series-title":"Lect Notes Comput Sci","volume-title":"Foundations of Software Technology and Theoretical Computer Science. Proceedings","author":"W. Reif","year":"1992","unstructured":"W. Reif. Verification of Large Software Systems. In R. Shyamasundar, editor, Foundations of Software Technology and Theoretical Computer Science. Proceedings. Springer LNCS 652, 1992."},{"key":"23_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0015471","volume-title":"KORSO: Methods, Languages, and Tools for the Construction of Correct Software-Final Report","author":"W. Reif","year":"1995","unstructured":"W. Reif. The KlV-approach to Software Verification. In M. Broy and S. J\u00e4hnichen, editors, KORSO: Methods, Languages, and Tools for the Construction of Correct Software-Final Report. Springer LNCS 1009, 1995."},{"key":"23_CR18","doi-asserted-by":"crossref","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.","DOI":"10.1109\/CMPASS.1995.521894"},{"key":"23_CR19","doi-asserted-by":"crossref","unstructured":"W. Reif, G. Schellhorn, K. Stenzel, and M. Balser. Structured specifications and interactive proofs with KIV. In W. Bibel and P. Schmitt, editors, Automated Deduction\u2014A Basis for Applications. Kluwer Academic Publishers, 1998.","DOI":"10.1007\/978-94-017-0435-9_1"},{"key":"23_CR20","series-title":"Lect Notes Comput Sci","volume-title":"Foundation of Software Technology and Theoretical Computer Science. Proceedings","author":"W. Reif","year":"1993","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, 1993."},{"key":"23_CR21","series-title":"Lect Notes Comput Sci","volume-title":"Coll. on Foundations of Computation Theory","author":"D. T. Sannella","year":"1983","unstructured":"D. T. Sannella 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."},{"key":"23_CR22","unstructured":"G. Schellhorn and W. Ahrendt. Reasoning about Abstract State Machines: The WAM Case Study. Journal of Universal Computer Science (J. UCS), 1997. available at \n                    http:\/\/hyperg.iicm.tu-graz.ac.at\/jucs\/\n                    \n                  ."}],"container-title":["Lecture Notes in Computer Science","Applied Formal Methods \u2014 FM-Trends 98"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48257-1_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,17]],"date-time":"2019-02-17T23:36:32Z","timestamp":1550446592000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48257-1_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664628","9783540482574"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-48257-1_23","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}