{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:07:06Z","timestamp":1725494826167},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540665885"},{"type":"electronic","value":"9783540481188"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48118-4_46","type":"book-chapter","created":{"date-parts":[[2007,11,14]],"date-time":"2007-11-14T01:30:57Z","timestamp":1195003857000},"page":"1816-1835","source":"Crossref","is-referenced-by-count":5,"title":["Secure synthesis of code: a process improvement experiment"],"prefix":"10.1007","author":[{"given":"P.","family":"Garbett","sequence":"first","affiliation":[]},{"given":"J. P.","family":"Parkes","sequence":"additional","affiliation":[]},{"given":"M.","family":"Shackleton","sequence":"additional","affiliation":[]},{"given":"S.","family":"Anderson","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[1999,9,17]]},"reference":[{"key":"46_CR1","unstructured":"Adelard. ASCAD-Adelard Safety Case Development Manual. Adelard, 1998. ISBN 0 9533771 0 5."},{"issue":"5","key":"46_CR2","doi-asserted-by":"publisher","first-page":"611","DOI":"10.1109\/32.24710","volume":"15","author":"G. Barrett","year":"1989","unstructured":"Geoff Barrett. Formal methods applied to a floating-point number systems. IEEE Transactions on Software Engineering, 15(5):611\u2013621, May 1989.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"46_CR3","unstructured":"B. A. Carre, D. L. Clutterbuck, C. W. Debney, and I. M. O'Neill. SPADE-the thampton Program Analysis and Development Environment. In Software Engineering Environments, pages 129\u2013134. Peter Peregrinus, 1986."},{"key":"46_CR4","unstructured":"P. Caseley, C. O'Halloran, and A. Smith. Explaining code with pictures-a case study. Technical Report DERA\/CIS\/CIS3\/TR990083\/1.0 (DRAFT), DERA, 1997."},{"key":"46_CR5","doi-asserted-by":"crossref","unstructured":"S. Easterbrook, R Lutz, R. Covington, J. Kelly, Y. Ampo, and D. Hamilton. Experiences using lightweight formal methods for requirements modeling. IEEE Transactions on Software Engineering, 24(1), Jan 1998.","DOI":"10.1109\/32.663994"},{"key":"46_CR6","first-page":"59","volume-title":"International Conference on Very Large Scale Integration","author":"E.M. Mayger","year":"1991","unstructured":"E.M. Mayger and M.P. Fourman. Integration of formal methods with system design. In A. Halaas and P.B. Denyer, editors, International Conference on Very Large Scale Integration, pages 59\u201370, Edinburgh, Scotland, August 1991. IFIP Transactions, North-Holland."},{"key":"46_CR7","unstructured":"M. P. Fourman. Formal System Design, chapter 5, pages 191\u2013236. North-Holland, 1990."},{"key":"46_CR8","unstructured":"P. Garbett, J. Parkes, M. Shackleton, and S. Anderson. A case study in innovative process improvement: Code synthesis from formal specifications. In Avionics 98, 1998."},{"key":"46_CR9","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/0164-1212(95)00077-1","volume":"34","author":"R. Lutz","year":"1996","unstructured":"R. Lutz. Targeting safety-related errors during software requirements analysis. The Journal of Systems and Software, 34:223\u2013230, Sept 1996.","journal-title":"The Journal of Systems and Software"},{"key":"46_CR10","volume-title":"The Definition of Standard ML","author":"R. Milner","year":"1989","unstructured":"Robin Milner, Mads Tofte, and Robert Harper. The Definition of Standard ML. MIT Press, Cambridge, MA, 1989."},{"key":"46_CR11","unstructured":"M.P. Fourman and E.M. Mayger. Formally Based System Design-Interactive hardware scheduling. In G. Musgrave and U. Lauther, editors, Very Large Scale Integration, pages 101\u2013112, Munich, Federal Republic of Germany, August 1989. IFIP TC 10\/WG10.5 International Conference, North-Holland."},{"key":"46_CR12","doi-asserted-by":"crossref","unstructured":"I.M. O'Neill, D.L. Clutterbuck, P.F. Farrow, P.G. Summers, and W.C. Dolman. The formal verification of safety critical assembly code. In Safety of Computer Control Systems, pages 115\u2013120. Pergammon Press, 1988.","DOI":"10.1016\/S1474-6670(17)54540-1"},{"key":"46_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A generic theorem prover","author":"L. C. Paulson","year":"1994","unstructured":"L. C. Paulson. Isabelle: A generic theorem prover. Lecture Notes in Computer Science, 828:xvii + 321, 1994."},{"key":"46_CR14","unstructured":"Requirements and Technical Concepts for Aviation. Software Considerations in Airborne Systems and Equipment Certification, Dec 1992. (document RTCA SC167\/DO-178B)."},{"key":"46_CR15","unstructured":"S. Finn, M.P. Fourman, and G. Musgrave. Interactive synthesis in HOL-abstract. In M. Archer, J.J. Joyce, K.N. Levitt, and P.J. Windley, editors, International Workshop on Higher Order Logic Theorem Proving and its Applications, Davis, California, August 1991. IEEE Computer Society, ACM SIGDA, IEEE Computer Society Press."},{"key":"46_CR16","unstructured":"S. Finn, M.P. Fourman, M.D. Francis, and B. Harris. Formal system design-interactive synthesis based on computer assisted formal reasoning. In Luc J. M. Claesen, editor, Applied Formal Methods For Correct VLSI Design, volume 1, pages 97\u2013110. IMEC-IFIP, Elsevier Science Publishers, 1989."},{"issue":"1","key":"46_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF02420941","volume":"5","author":"H. Saiedan","year":"1996","unstructured":"H. Saiedan and L. M. Mc Clanahan. Frameworks for quality software process: SEI capability maturity model. Software Quality Journal, 5(1):1, 1996.","journal-title":"Software Quality Journal"}],"container-title":["Lecture Notes in Computer Science","FM\u201999 \u2014 Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48118-4_46","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,25]],"date-time":"2019-02-25T11:00:37Z","timestamp":1551092437000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48118-4_46"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665885","9783540481188"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-48118-4_46","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}