{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:08:31Z","timestamp":1725516511208},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540691471"},{"type":"electronic","value":"9783540691495"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-69149-5_20","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T12:07:43Z","timestamp":1218542863000},"page":"182-188","source":"Crossref","is-referenced-by-count":11,"title":["Generating Programs Plus Proofs by Refinement"],"prefix":"10.1007","author":[{"given":"Douglas R.","family":"Smith","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"20_CR1","unstructured":"Becker, M., Gilham, L., Smith, D.\u00a0R. Planware II: Synthesis of schedulers for complex resource systems. Tech. rep. Kestrel Technology (2003)"},{"key":"20_CR2","volume-title":"Software Engineering Economics","author":"B. Boehm","year":"1981","unstructured":"Boehm, B.: Software Engineering Economics. Prentice-Hall, Englewood Cliffs (1981)"},{"key":"20_CR3","unstructured":"Coglio, A.: Toward automatic generation of provably correct Java Card applets. In: Proc. 5th ECOOP Workshop on Formal Techniques for Java-like Programs (July 2003)"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"Green, C.: Application of theorem proving to problem solving. In: Proceedings of the First International Joint Conference on Artificial Intelligence, pp. 219\u2013239 (1969)","DOI":"10.21236\/ADA459656"},{"key":"20_CR5","unstructured":"Green, C., Westfold, S.: Experiments suggest high level formal models and automated code synthesis significantly increase dependability. Tech. Rep. KES.U.00.8, Kestrel Institute (January 2001)"},{"key":"20_CR6","unstructured":"Kestrel Institute. Specware System and documentation (2003), http:\/\/www.specware.org\/"},{"issue":"1","key":"20_CR7","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1145\/357084.357090","volume":"2","author":"Z. Manna","year":"1980","unstructured":"Manna, Z., Waldinger, R.: A deductive approach to program synthesis. ACM Transactions on Programming Languages and Systems\u00a02(1), 90\u2013121 (1980)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"20_CR8","first-page":"157","volume-title":"Proceedings of Sixteenth International Conference on Automated Software Engineering","author":"D. Pavlovic","year":"2001","unstructured":"Pavlovic, D., Smith, D.R.: Composition and refinement of behavioral specifications. In: Proceedings of Sixteenth International Conference on Automated Software Engineering, pp. 157\u2013165. IEEE Computer Society Press, Los Alamitos (2001)"},{"issue":"9","key":"20_CR9","doi-asserted-by":"publisher","first-page":"1024","DOI":"10.1109\/32.58788","volume":"16","author":"D.R. Smith","year":"1990","unstructured":"Smith, D.R.: KIDS \u2013 a semi-automatic program development system. IEEE Transactions on Software Engineering Special Issue on Formal Methods in Software Engineering\u00a016(9), 1024\u20131043 (1990)","journal-title":"IEEE Transactions on Software Engineering Special Issue on Formal Methods in Software Engineering"},{"issue":"5-6","key":"20_CR10","doi-asserted-by":"publisher","first-page":"571","DOI":"10.1016\/S0747-7171(06)80006-4","volume":"15","author":"D.R. Smith","year":"1993","unstructured":"Smith, D.R.: Constructing specification morphisms. Journal of Symbolic Computation, Special Issue on Automatic Programming\u00a015(5-6), 571\u2013606 (1993)","journal-title":"Journal of Symbolic Computation, Special Issue on Automatic Programming"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/BFb0014308","volume-title":"Algebraic Methodology and Software Technology","author":"D.R. Smith","year":"1996","unstructured":"Smith, D.R.: Toward a classification approach to design. In: Nivat, M., Wirsing, M. (eds.) AMAST 1996. LNCS, vol.\u00a01101, pp. 62\u201384. Springer, Heidelberg (1996)"},{"key":"20_CR12","first-page":"251","volume-title":"Calculational System Design, Proceedings of the NATO Advanced Study Institute","author":"D.R. Smith","year":"1999","unstructured":"Smith, D.R.: Mechanizing the development of software. In: Broy, M., Steinbrueggen, R. (eds.) Calculational System Design, Proceedings of the NATO Advanced Study Institute, pp. 251\u2013292. IOS Press, Amsterdam (1999)"},{"issue":"2-3","key":"20_CR13","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1016\/0167-6423(90)90025-9","volume":"14","author":"D.R. Smith","year":"1990","unstructured":"Smith, D.R., Lowry, M.R.: Algorithm theories and design tactics. Science of Computer Programming\u00a014( 2-3), 305\u2013321 (1990)","journal-title":"Science of Computer Programming"},{"key":"20_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1007\/3-540-45614-7_25","volume-title":"FME 2002: Formal Methods - Getting IT Right","author":"M. Whalen","year":"2002","unstructured":"Whalen, M., Schumann, J., Fischer, B.: Synthesizing certified code. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol.\u00a02391, pp. 431\u2013450. Springer, Heidelberg (2002)"},{"key":"20_CR15","doi-asserted-by":"crossref","unstructured":"Whittle, J., Schumann, J. Automating the implementation of Kalman filter algorithms. Tech. rep. NASA Ames Automated Software Engineering Group(submitted, 2004)","DOI":"10.1145\/1039813.1039816"},{"key":"20_CR16","first-page":"87","volume-title":"Proceedings of the International Conference on Software Engineering 2000","author":"J. Widmaier","year":"2000","unstructured":"Widmaier, J., Schmidts, C., Huang, X.: Producing more reliable software: Mature software engineering process vs. state-of-the-art technology? In: Proceedings of the International Conference on Software Engineering 2000, Limerick, Ireland, pp. 87\u201392. ACM Press, New York (2000)"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69149-5_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T03:42:46Z","timestamp":1557718966000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69149-5_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540691471","9783540691495"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69149-5_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}