{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T07:41:00Z","timestamp":1725608460416},"publisher-location":"Vienna","reference-count":43,"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_1","type":"book-chapter","created":{"date-parts":[[2011,9,15]],"date-time":"2011-09-15T07:42:02Z","timestamp":1316072522000},"page":"1-17","source":"Crossref","is-referenced-by-count":0,"title":["Formal Methods and Tools: Introduction and Overview"],"prefix":"10.1007","author":[{"given":"R.","family":"Berghammer","sequence":"first","affiliation":[]},{"given":"Y.","family":"Lakhnech","sequence":"additional","affiliation":[]},{"given":"W.","family":"Reif","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","volume-title":"Lecture notes in computer science, vol 600","author":"R Alur","year":"1991","unstructured":"Alur R., Henzinger T.A. (1991): Logics and models of real-time: A survey. In: Proc. of the REX workshop \u201cReal-time: Theory and practice\u201d. Springer, Berlin, pp. 74\u2013106 (Lecture notes in computer science, vol. 600)"},{"key":"1_CR2","volume-title":"A computational logic","author":"RS Boyer","year":"1979","unstructured":"Boyer R.S., Moore J.S. (1979): A computational logic. Academic Press, New York"},{"key":"1_CR3","unstructured":"de Bruijn N.G. (1980): A survey of the project AUTOMATH. In: Essays on combina-tory logic, lambda calculus and formalism. Academic Press, London, pp. 580\u2013606"},{"issue":"2","key":"1_CR4","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"JR Burch","year":"1992","unstructured":"Burch J.R., Clarke E.M., McMillan K.L., Dill D.L., Hwang L.J. (1992): Symbolic model checking: 1020 states and byond. Information and computation 98 (2), pp. 142\u2013170","journal-title":"Information and computation"},{"key":"1_CR5","volume-title":"Lecture notes in computer science, vol 131","author":"E Clarke","year":"1982","unstructured":"Clarke E., Emerson E.A. (1982): Design and synthesis of synchronization skeletonsusing branching time temporal logic. In: Proc. Workshop \u201cLogics of programs\u201d.Springer, Berlin, pp. 52\u201371 (Lecture notes in computer science, vol. 131)"},{"key":"1_CR6","volume-title":"Lecture notesin computer science, vol 803","author":"E Clarke","year":"1993","unstructured":"Clarke E., Grumberg O, Long D. (1993): Verification tools for finite-state concurrentsystems. In: A decade of concurrency. Springer, Berlin, pp. 124\u2013175 (Lecture notesin computer science, vol. 803)"},{"key":"1_CR7","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/3-540-11492-0","volume-title":"An introduction to the PL\/CV2 programming logic","author":"RL Constable","year":"1982","unstructured":"Constable R.L., Johnson S.D., Eichenlaub C.D. (1982): An introduction to the PL\/CV2 programming logic. Springer, Berlin (Lecture notes in computer science, vol. 135 )"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Constable R.L., Knoblock T.B:, Bates J.L. (1985): Writing programs that construct","DOI":"10.1007\/BF00244273"},{"key":"1_CR9","unstructured":"proofs. Journal of Automated Reasoning 1 (3), pp. 285\u2013326"},{"key":"1_CR10","volume-title":"Implementing mathematics with the Nuprl proof development system","author":"RL Constable","year":"1986","unstructured":"Constable R.L., Allen S.F., Bromley H.M., Cleaveland W.R., Cremer J.F., Harper R.W., Howe D.J., Knoblock T.B., Mendier N.P., Panagaden P., Sasaki, J.T., Smith, S.F. (1986): Implementing mathematics with the Nuprl proof development system. Prentice-Hall, London"},{"key":"1_CR11","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"EW Dijkstra","year":"1975","unstructured":"Dijkstra E.W. (1975): Guarded commands, nondeterminacy and formal derivation of programs. Comm. ACM 18, pp. 453\u2013457","journal-title":"Comm. ACM"},{"key":"1_CR12","volume-title":"A discipline of programming","author":"EW Dijkstra","year":"1976","unstructured":"Dijkstra E.W. (1976): A discipline of programming. Prentice-Hall, London"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Emerson E.A. (1990): Temporal and modal logic. In: Handbook of theoretical computer science, vol. B. Elsevier, Amsterdam, pp. 995\u20131072","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"1_CR14","volume-title":"Proc. of the 13th international conference on automated deduction. Springer, Berlin, pp. 298-302 (Lecture notes in artificial intelligence, vol","author":"WM Farmer","year":"1104","unstructured":"Farmer W.M., Guttman J.D., F\u00e4brega F.J.T. (1996): IMPS: An updated description. In: Proc. of the 13th international conference on automated deduction. Springer, Berlin, pp. 298\u2013302 (Lecture notes in artificial intelligence, vol. 1104 )"},{"key":"1_CR15","volume-title":"Digital Equipment Corporation","author":"SJ Garland","year":"1995","unstructured":"Garland S.J., Guttag J.V. (1995): A Guide to LP, the Larch Prover. Systems research report 82, Digital Equipment Corporation"},{"key":"1_CR16","doi-asserted-by":"crossref","first-page":"78","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF: A mechanised logic of computation","author":"M Gordon","year":"1979","unstructured":"Gordon M., Milner R., Wadsworth C. (1979): Edinburgh LCF: A mechanised logic of computation. Springer, Berlin (Lecture notes in computer science, vol. 78 )"},{"key":"1_CR17","volume-title":"In: VLSI","author":"M Gordon","year":"1988","unstructured":"Gordon M. (1988): HOL: A proof generating system for higher-order logic. In: VLSI"},{"key":"1_CR18","unstructured":"specification and synthesis. Kluwer, Amsterdam, pp. 73\u2013128"},{"key":"1_CR19","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-5983-1","volume-title":"The science of computer programming","author":"D Gries","year":"1981","unstructured":"Gries D. (1981): The science of computer programming. Springer, Berlin"},{"key":"1_CR20","volume-title":"Ph","author":"JV Guttag","year":"1975","unstructured":"Guttag J.V. (1975): The specification and application to programming of abstract data types. Ph. D. thesis, Univ. of Toronto"},{"key":"1_CR21","volume-title":"In: Applications of algebraic specifications using OBJ","author":"J Goguen","year":"1992","unstructured":"Goguen J., Winkler T., Meseguer J., Futatsugi K., Jouannaud J.-P. (1992): Introducing OBJ. In: Applications of algebraic specifications using OBJ. Cambridge University Press, Cambridge"},{"key":"1_CR22","first-page":"583","volume":"576580","author":"CAR Hoare","year":"1969","unstructured":"Hoare C.A.R. (1969): An axiomatic basis for computer programming. Comm. ACM 12, pp. 576\u2013580, 583","journal-title":"Comm. ACM 12, pp"},{"key":"1_CR23","volume-title":"Design and validation of protocols","author":"GJ Holzmann","year":"1990","unstructured":"Holzmann G.J. (1990): Design and validation of protocols. Prentice-Hall, London"},{"key":"1_CR24","volume-title":"BISS mono-graphs, vol 1","author":"H-M H\u00f6rcher","year":"1998","unstructured":"H\u00f6rcher H.-M., Mikk E (1998): Test automation using Z specifications. In: Tools for system development and verification. Shaker, Aachen, pp. 107\u2013119 (BISS mono-graphs, vol. 1)"},{"key":"1_CR25","volume-title":"INRIA","author":"G Huet","year":"1997","unstructured":"Huet G., Kahn G., Pauling-Mohring Ch. (1997): The coq proof assistant. Technical Report 178, INRIA"},{"key":"1_CR26","first-page":"31","volume-title":"About the nature of computer science. Colloquium, Fachbereich Informatik","author":"J Hartmanis","year":"1994","unstructured":"Hartmanis J. (1994) About the nature of computer science. Colloquium, Fachbereich Informatik, Universit\u00e4t Hamburg, January 31"},{"key":"1_CR27","unstructured":"Jones C.B. (1990): Systematic software development using VDM. Second edition, Prentice-Hall, London"},{"issue":"4","key":"1_CR28","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1109\/32.588534","volume":"23","author":"M Kaufmann","year":"1997","unstructured":"Kaufmann M., Moore J.S. (1997): An industrial strength theorem prover for a logic based on Commom Lisp. IEEE Transactions on Software Engineering 23 (4), pp. 203\u2013213","journal-title":"IEEE Transactions on Software Engineering"},{"key":"1_CR29","volume-title":"Lecture notes in computer science, vol 806","author":"L Magnusson","year":"1994","unstructured":"Magnusson L., Nordstr\u00f6m B. (1994): The ALF proof editor and its proof engine. In: Types for proofs and programs. Springer, Berlin, pp. 213\u2013237 (Lecture notes in computer science, vol. 806)"},{"key":"1_CR30","volume-title":"On the refinement calculus","author":"C Morgan","year":"1992","unstructured":"Morgan C, Vickers T. (1992): On the refinement calculus. Springer, Berlin"},{"issue":"2","key":"1_CR31","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S Owre","year":"1995","unstructured":"Owre S., Rushby J., Shankar N., von Henke F. (1995): Formal verification for fault-tolerant architectures: Prolegoena to the design of PVS. IEEE Transactions on Software Engineering, 21 (2), pp. 107\u2013125","journal-title":"IEEE Transactions on Software Engineering"},{"key":"1_CR32","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1017\/CBO9780511526602","volume-title":"Logic and computation","author":"LC Paulson","year":"1987","unstructured":"Paulson L.C. (1987): Logic and computation. Cambridge University Press, Cambridge (Cambridge tracts in theoretical computer science, vol. 2 )"},{"key":"1_CR33","doi-asserted-by":"crossref","first-page":"828","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A generic theorem prover","author":"LC Paulson","year":"1994","unstructured":"Paulson L.C. (1994): Isabelle: A generic theorem prover. Springer, Berlin (Lecture notes in computer science, vol. 828 )"},{"key":"1_CR34","doi-asserted-by":"crossref","unstructured":"Pnueli A. (1977): The temporal logic of programs. In: Proc. of the 18th Ann. Symp. On Foundations of computer science, IEEE Computer Society, Providence, pp. 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"1_CR35","doi-asserted-by":"publisher","DOI":"10.1093\/acprof:oso\/9780198243113.001.0001","volume-title":"Past present and future","author":"P Prior","year":"1967","unstructured":"Prior P. (1967): Past, present, and future. Oxford University Press, Oxford"},{"key":"1_CR36","volume-title":"Lecture notes in computer science, vol 137","author":"JP Queille","year":"1982","unstructured":"Queille J.P., Sifakis J. (1982): Specification and verification of concurrent programs inC\u00c9SAR. In: Proc. of the 5th Intern. Symp. on Programming, Springer, Berlin, pp.195\u2013220 (Lecture notes in computer science, vol. 137)"},{"key":"1_CR37","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1007\/978-94-017-0435-9_1","volume-title":"h2: Automated deduction: A basis for applications","author":"W Reif","year":"1998","unstructured":"Reif W., Schellhoru G., Stenzel K., Balser M. (1998): Structural specifications and interactive proofs in KIV. h2: Automated deduction: A basis for applications, vol. II. Kluwer, Amsterdam, pp. 13\u201339"},{"key":"1_CR38","unstructured":"Spivey J.M. (1992): The Z notation: a reference manual. Second edition, Prentice-Hall, London"},{"key":"1_CR39","doi-asserted-by":"crossref","unstructured":"Thomas W. (1990): Automata on infinite objects. In: Handbook of theoretical computer science, vol. B. Elsevier, Amsterdam, pp. 134\u2013191.","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"1_CR40","doi-asserted-by":"crossref","unstructured":"Wirsing M. (1990): Algebraic specifications. In: Handbook of theoretical computer science, vol. B, Elsevier, Amsterdam, pp. 675\u2013788.","DOI":"10.1016\/B978-0-444-88074-1.50018-4"},{"key":"1_CR41","doi-asserted-by":"crossref","unstructured":"Weyhrauch R. (1981): Prolegomena to a theory of mechanized formal reasoning. In: Readings in artifical intelligence. Tioga, Palo Alto, pp. 173\u2013191","DOI":"10.1016\/B978-0-934613-03-3.50016-7"},{"key":"1_CR42","volume-title":"Using Z: specification, refinement and proof","author":"J Woodcock","year":"1996","unstructured":"Woodcock J., Davis J. (1996): Using Z: specification, refinement, and proof. Prentice-Hall, London"},{"key":"1_CR43","first-page":"119","volume-title":"Algebraic specification of data types. Computation structures group memo","author":"SN Zilles","year":"1974","unstructured":"Zilles S.N. (1974): Algebraic specification of data types. Computation structures group memo 119, Laboratory of computer science, MIT"}],"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_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,23]],"date-time":"2020-11-23T09:36:02Z","timestamp":1606124162000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-7091-6355-9_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783211832820","9783709163559"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-7091-6355-9_1","relation":{},"subject":[],"published":{"date-parts":[[1999]]}}}