{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,2]],"date-time":"2025-03-02T05:45:50Z","timestamp":1740894350144,"version":"3.38.0"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540204619"},{"type":"electronic","value":"9783540398936"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-39893-6_2","type":"book-chapter","created":{"date-parts":[[2011,1,7]],"date-time":"2011-01-07T15:35:57Z","timestamp":1294414557000},"page":"16-25","source":"Crossref","is-referenced-by-count":2,"title":["Model Based Code Verification"],"prefix":"10.1007","author":[{"given":"Colin","family":"O\u2019Halloran","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","unstructured":"Stepney, S.: High Integrity Compilation"},{"key":"2_CR2","volume-title":"High integrity Ada, The SPARK approach","author":"J. Barnes","year":"1997","unstructured":"Barnes, J.: High integrity Ada, The SPARK approach. Addison-Wesley, Reading (1997)"},{"key":"2_CR3","unstructured":"Pygott, C.: Formal Specification of the VIPER microprocessor in HOL, RSRE report 90009"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Cohn, A.: The notion of proof in hardware verification. Journal of automated reasoning\u00a05, 127\u2013139","DOI":"10.1007\/BF00243000"},{"key":"2_CR5","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/BF01211435","volume":"3","author":"S. Stepney","year":"1991","unstructured":"Stepney, S., Whitley, D., Cooper, D., Grant, C.: A demonstrably correct compiler. BCS Formal Aspects of Computing\u00a03, 58\u2013101 (1991)","journal-title":"BCS Formal Aspects of Computing"},{"key":"2_CR6","unstructured":"Stepney, S.: Incremental development of a high integrity compiler: experience from an industrial development. In: Third IEEE High-Assurance Systems Engineering Symposium (HASE 1998), Washington DC (1998)"},{"key":"2_CR7","unstructured":"Davies, J., Woodcock, J.: Using Z. Prentice Hall International series in computer science (1996)"},{"key":"2_CR8","unstructured":"http:\/\/www.info.uni-karlsruhe.de\/~erifix\/index.html"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","volume-title":"FME \u201994: Industrial Benefit of Formal Methods","author":"A.C. Storey","year":"1994","unstructured":"Storey, A.C., Haughton, H.P.: A strategy for the production of verifiable code using the B method. In: Naftalin, M., Bertr\u00e1n, M., Denvir, T. (eds.) FME 1994. LNCS, vol.\u00a0873. Springer, Heidelberg (1994)"},{"key":"2_CR10","volume-title":"12th IEEE ASE","author":"A. Armando","year":"1997","unstructured":"Armando, A., Smaill, A., Green, I.: Automatic Synthesis of Recursive Programs: The Proof-Planning Paradigm. In: 12th IEEE ASE. IEEE Computer Society Press, Los Alamitos (1997)"},{"key":"2_CR11","unstructured":"Morgan, C.: Programming from specifications. Prentice-Hall International series in computer science (1990)"},{"key":"2_CR12","volume-title":"14th IEEE ASE","author":"E. Tronci","year":"1999","unstructured":"Tronci, E.: Automatic synthesis of control software for an industrial automation control system. In: 14th IEEE ASE. IEEE Computer Society Press, Los Alamitos (1999)"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1816","DOI":"10.1007\/3-540-48118-4_46","volume-title":"FM\u201999 - Formal Methods","author":"P. Garbett","year":"1999","unstructured":"Garbett, P., Parkes, J., Shackleton, M., Anderson, S.: Secure synthesis of code: a process improvement experiment. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol.\u00a01709, p. 1816. Springer, Heidelberg (1999)"},{"key":"2_CR14","unstructured":"O\u2019Halloran, C.: Acceptance Based Assurance. In: Proceedings of the IEEE conference on Automated Software Engineering 2001 (2001)"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Poppleton, M., Banach, R.: Retrenchment: Extending the Reach of Refinement. In: Proceedings of IEEE conference on Automated Software Engineering 1999, pp. 158\u2013165 (1999)","DOI":"10.1109\/ASE.1999.802189"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/3-540-36580-X_11","volume-title":"Hybrid Systems: Computation and Control","author":"J. Boulton Richard","year":"2003","unstructured":"Boulton Richard, J., Hardy, R., Martin, U.: A Hoare Logic for Single-Input Single-Output Continuous-Time Control Systems. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol.\u00a02623, pp. 113\u2013125. Springer, Heidelberg (2003)"},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/3-540-45648-1_21","volume-title":"ZB 2002: Formal Specification and Development in Z and B","author":"J. Blow","year":"2002","unstructured":"Blow, J., Galloway, A.: Generalised Substitution Language and Differentials. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol.\u00a02272, pp. 396\u2013415. Springer, Heidelberg (2002)"},{"key":"2_CR18","unstructured":"Davies, J., Crichton, C.: Concurrency and refinement in the UML. ENTCS\u00a070(3) (2002)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-39893-6_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,1]],"date-time":"2025-03-01T14:26:23Z","timestamp":1740839183000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39893-6_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540204619","9783540398936"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39893-6_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}