{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,7]],"date-time":"2025-10-07T05:17:39Z","timestamp":1759814259771},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540297970"},{"type":"electronic","value":"9783540322504"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11576280_32","type":"book-chapter","created":{"date-parts":[[2005,10,24]],"date-time":"2005-10-24T14:01:26Z","timestamp":1130162486000},"page":"465-479","source":"Crossref","is-referenced-by-count":17,"title":["ClawZ: Cost-Effective Formal Verification for Control Systems"],"prefix":"10.1007","author":[{"given":"M. M.","family":"Adams","sequence":"first","affiliation":[]},{"given":"P. B.","family":"Clayton","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"32_CR1","unstructured":"The Mathworks Inc.: Using Simulink. 5th edn. (2002)"},{"key":"32_CR2","unstructured":"TA Consultancy Services Ltd.: MALPAS Training Course Notes, 2nd edn. (1995)"},{"key":"32_CR3","volume-title":"Using Z: Specification, Refinement and Proof","author":"J. Woodcock","year":"1996","unstructured":"Woodcock, J., Davies, J.: Using Z: Specification, Refinement and Proof, 1st edn. Prentice Hall, Englewood Cliffs (1996)","edition":"1"},{"key":"32_CR4","unstructured":"Lemma 1 Ltd. website, \n                    \n                      http:\/\/www.lemma-one.com"},{"volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher Order Logic","year":"1993","key":"32_CR5","unstructured":"Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)"},{"key":"32_CR6","volume-title":"14th IEEE ASE","author":"C. O\u2019Halloran","year":"1999","unstructured":"O\u2019Halloran, C., Smith, A.: Verification of Picture Generated Code. In: 14th IEEE ASE. IEEE Computer Society Press, Los Alamitos (1999)"},{"key":"32_CR7","volume-title":"13th IEEE ASE","author":"C. O\u2019Halloran","year":"1998","unstructured":"O\u2019Halloran, C., Smith, A.: Don\u2019t Verify, Abstract! In: 13th IEEE ASE. IEEE Computer Society Press, Los Alamitos (1998)"},{"key":"32_CR8","volume-title":"Programming from Specifications","author":"C. Morgan","year":"1994","unstructured":"Morgan, C.: Programming from Specifications, 2nd edn. Prentice Hall, Englewood Cliffs (1994)","edition":"2"},{"key":"32_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF","author":"M. Gordon","year":"1979","unstructured":"Gordon, M., Milner, A., Wadsworth, C.: Edinburgh LCF \u2013 A Mechanical Logic of Computation. In: Gordon, M., Wadsworth, C.P., Milner, R. (eds.) Edinburgh LCF. LNCS, vol.\u00a078, Springer, Heidelberg (1979)"},{"key":"32_CR10","unstructured":"Harrison, J.: Metatheory and Reflection in Theorem Proving: A Survey Critique. Technical report, University of Cambridge Computer Laboratory (1995)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11576280_32.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:44:22Z","timestamp":1619505862000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11576280_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540297970","9783540322504"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/11576280_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}