{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T07:40:59Z","timestamp":1725608459412},"publisher-location":"Vienna","reference-count":20,"publisher":"Springer Vienna","isbn-type":[{"type":"print","value":"9783211832820"},{"type":"electronic","value":"9783709163559"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/978-3-7091-6355-9_14","type":"book-chapter","created":{"date-parts":[[2011,9,15]],"date-time":"2011-09-15T03:42:02Z","timestamp":1316058122000},"page":"189-200","source":"Crossref","is-referenced-by-count":0,"title":["Towards Light-Weight Verification and Heavy-Weight Testing"],"prefix":"10.1007","author":[{"given":"Stephan","family":"Pfab","sequence":"first","affiliation":[]},{"given":"Harald","family":"Rue\u00df","sequence":"additional","affiliation":[]},{"given":"Sam","family":"Owre","sequence":"additional","affiliation":[]},{"given":"Friedrich W.","family":"von Henke","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1109\/LICS.1991.151645","volume-title":"Proceedings, Sixth Annual IEEE Symposium On Logic in Computer Science","author":"U Berger","year":"1991","unstructured":"U. Berger and H. Schwichtenberg (1991): An inverse of the evaluation functional for typed A-calculus. In Proceedings, Sixth Annual IEEE Symposium On Logic in Computer Science, pages 203\u2013211, Amsterdam, The Netherlands. IEEE Computer Society Press."},{"key":"14_CR2","volume-title":"A Correctness Proof for Pipelining in RISC Architectures","author":"E B\u00f6rger","year":"1996","unstructured":"E. B\u00f6rger and S. Mazzanti (1996): A Correctness Proof for Pipelining in RISC Architectures. Technical Report DIMACS 96\u201322, Dipartimento di Informatica, University of Pisa, Corso Italia 40, 56125 Pisa, Italy."},{"key":"14_CR3","volume-title":"Automated Reasoning and Its Applications: Essays in Honor of Larry Wos","author":"RS Boyer","year":"1996","unstructured":"R.S. Boyer and J S. Moore (1996): Mechanized Formal Reasoning about Programs and Computing Machines. In Automated Reasoning and Its Applications: Essays in Honor of Larry Wos. MIT Press."},{"key":"14_CR4","volume-title":"The Coq Proof Assistant User\u2019s Guide (Version 5.8)","author":"G Dowek","year":"1993","unstructured":"G. Dowek, A. Felty, H. Herbelin, G. Huet, Ch. Murthy, C. Parent, Chr. PaulinMohring, and B. Werner (1993): The Coq Proof Assistant User\u2019s Guide (Version 5.8). INRIA-Rocquencourt - CNRS - ENS Lyon. Projet Formel."},{"key":"14_CR5","first-page":"9","volume-title":"Current Trends in Theoretical Computer Science","author":"Y Gurevich","year":"1995","unstructured":"Y. Gurevich (1995): Evolving algebras 1993: Lipari guide. In E. B\u00f6rger, editor, Current Trends in Theoretical Computer Science, pages 9\u201336. Computer Science Press."},{"key":"14_CR6","volume-title":"CAV\u201998:Computer-Aided Verification","author":"D Hardin","year":"1998","unstructured":"D. Hardin, M. Wilding, and D. Greve (1998): Transforming the Theorem Prover into a Digital Design Tool: From Concept Car to Off-Road Vehicle. In CAV\u201998: Computer-Aided Verification, Lecture Notes in Computer Science. Springer Verlag."},{"key":"14_CR7","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1145\/158511.158524","volume-title":"ACM Symposium on Principles of Programming Languages (POPL\u201993)","author":"SL Peyton","year":"1993","unstructured":"S.L. Peyton, Jones and Ph. Wader (1993): Imperative Functional Programming In ACM Symposium on Principles of Programming Languages (POPL\u201993),pages 71\u201384, Charleston."},{"issue":"4","key":"14_CR8","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1109\/32.588534","volume":"21","author":"M Kaufmann","year":"1997","unstructured":"M. Kaufmann and J S. Moore (1997): An Industrial Strength Theorem Prover for a Logic based on Common Lisp. IEEE Transactions on Software Engineering, 21(4):203\u2013213.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"14_CR9","volume-title":"Formal Methods in Computer-Aided Design (FMCAD \u201888)","author":"JS Moore","year":"1998","unstructured":"J S. Moore (1998): Symbolic Simulation: an ACL2 Approach. In Formal Methods in Computer-Aided Design (FMCAD \u201888), Lecture Notes in Computer Science. Springer Verlag. Accepted for publication."},{"issue":"2","key":"14_CR10","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S Owre","year":"1995","unstructured":"S. Owre, J. Rushby, N. Shankar, and F. von Henke (1995): Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS. IEEE Transactions on Software Engineering,21(2):107\u2013125.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"14_CR11","volume-title":"The PVS Specification Language, Version 2.2","author":"S Owre","year":"1998","unstructured":"S. Owre, N. Shankar, J.M. Rushby, and D.W.J Stringer-Calvert (1998): The PVS Specification Language, Version 2.2. Computer Science Lab, SRI International, Menlo Park CA 94025. From: \n                  http:\/\/www.csl.sri.com\/pvs.html\n                  \n                ."},{"key":"14_CR12","volume-title":"Mechanized Semantics of Simple Imperative Programming Constructs","author":"H Pfeifer","year":"1996","unstructured":"H. Pfeifer, A. Dold, F. W. v. Henke, and H. Rue\u00df (1996): Mechanized Semantics of Simple Imperative Programming Constructs. Ulmer Informatik-Berichte 96\u201311, Universit\u00e4t Ulm, Fakult\u00e4t f\u00fcr Informatik."},{"key":"14_CR13","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/3-540-59293-8_189","volume-title":"TAPSOFT\u201995: Theory and Practice of Software Development","author":"V Pratt","year":"1995","unstructured":"V. Pratt (1995) Anatomy of the Pentium Bug. In P.D. Mosses, M. Nielsen, and M.I. Schwartzbach, editors, TAPSOFT\u201995: Theory and Practice of Software Development, number 915 in Lecture Notes in Computer Science, pages 97\u2013107. Springer Verlag."},{"key":"14_CR14","unstructured":"N. Shankar (1998): Personal communication."},{"key":"14_CR15","first-page":"125","volume-title":"Applications of Formal Methods, International Series in Computer Science, chapter 7","author":"MK Srivas","year":"1995","unstructured":"M.K. Srivas and S.P. Miller (1995): Formal Verification of the AAMP5 Microprocessor. In M.G. Hinchey and J.P. Bowen, editors, Applications of Formal Methods, International Series in Computer Science, chapter 7, pages 125\u2013180. Prentice Hall, Hemel Hempstead, UK."},{"key":"14_CR16","first-page":"156","volume-title":"Formal Hardware Verification Methods and Systems in Comparison, volume 1287 of Lecture Notes in Computer Science","author":"M Srivas","year":"1997","unstructured":"M. Srivas, H. Rue\u00df, and D. Cyrluk (1997) Hardware Verification using PVS. In Th. Kropf, editor, Formal Hardware Verification Methods and Systems in Comparison, volume 1287 of Lecture Notes in Computer Science, chapter 4, pages 156\u2013205. Springer Verlag."},{"key":"14_CR17","volume-title":"Formale Verifikation des DLX RISC-Prozessors: Eine Fallstudie basierend auf abstrakten Zustandsmaschinen","author":"M Stegm\u00fcller","year":"1998","unstructured":"M. Stegm\u00fcller (1998): Formale Verifikation des DLX RISC-Prozessors: Eine Fallstudie basierend auf abstrakten Zustandsmaschinen. Master\u2019s thesis, Universit\u00e4t Ulm. From \n                  http:\/\/www.informatik.uni\n                  \n                -ulm.de\/ki\/Edu\/Diplomarbeiten."},{"key":"14_CR18","first-page":"604","volume-title":"Proceedings AMAST\u201996","author":"FW Henke von","year":"1996","unstructured":"F.W. von Henke, M. Luther, H. Pfeifer, H. Rue\u00df, D. Schwier, M. Strecker, and M. Wagner (1996): The TYPELAB specification and verification environment. In M. Nivat M. Wirsing, editor, Proceedings AMAST\u201996, pages 604\u2013607. Springer LNCS 1101."},{"key":"14_CR19","volume-title":"Proc. Intl. Conf. on Theorem Proving in Higher Order Logics","author":"FW Henke von","year":"1998","unstructured":"Friedrich W. von Henke, Stephan Pfab, Holger Pfeifer, and Harald Rue\u00df (1998): Case Studies in Meta-Level Theorem Proving. In Jim Grundy and Malcolm Newey, editors, Proc. Intl. Conf. on Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science. Springer-Verlag."},{"key":"14_CR20","volume-title":"Robust Computer System Proofs in PVS","author":"M Wilding","year":"1997","unstructured":"M. Wilding (1997): Robust Computer System Proofs in PVS. Presented at LFM\u201997: the Fourth NASA Langley Formal Methods Workshop; also available from \n                  http:\/\/www.csl.sri.com\n                  \n                \/sri-csl-fm.html."}],"container-title":["Tool Support for System Specification, Development and Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-7091-6355-9_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,10,8]],"date-time":"2018-10-08T20:51:56Z","timestamp":1539031916000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-7091-6355-9_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783211832820","9783709163559"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-7091-6355-9_14","relation":{},"subject":[],"published":{"date-parts":[[1999]]}}}