{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T00:58:34Z","timestamp":1725843514215},"publisher-location":"Cham","reference-count":17,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319274355"},{"type":"electronic","value":"9783319274362"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-27436-2_15","type":"book-chapter","created":{"date-parts":[[2015,12,16]],"date-time":"2015-12-16T02:06:46Z","timestamp":1450231606000},"page":"244-258","source":"Crossref","is-referenced-by-count":2,"title":["Combining Top-Down and Bottom-Up Techniques in Program Derivation"],"prefix":"10.1007","author":[{"given":"Dipak L.","family":"Chaudhari","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Om","family":"Damani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,12,17]]},"reference":[{"key":"15_CR1","series-title":"Graduate Texts in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1674-2","volume-title":"Refinement Calculus: A Systematic Introduction","author":"RJ Back","year":"1998","unstructured":"Back, R.J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science. Springer, Berlin (1998)"},{"key":"15_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/11783596_7","volume-title":"Mathematics of Program Construction","author":"R Backhouse","year":"2006","unstructured":"Backhouse, R., Michaelis, D.: Exercises in quantifier manipulation. In: Uustalu, T. (ed.) MPC 2006. LNCS, vol. 4014, pp. 69\u201381. Springer, Heidelberg (2006)"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-540-73368-3_34","volume-title":"Computer Aided Verification","author":"CW Barrett","year":"2007","unstructured":"Barrett, C.W., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 298\u2013302. Springer, Heidelberg (2007)"},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0105399","volume-title":"Theorem Proving in Higher Order Logics","author":"M Butler","year":"1996","unstructured":"Butler, M., L\u00e5ngbacka, T.: Program derivation using the refinement calculator. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol. 1125. Springer, Heidelberg (1996)"},{"key":"15_CR5","unstructured":"Carrington, D., Hayes, I., Nickson, R., Watson, G.N., Welsh, J.: A tool for developing correct programs by refinement. Technical report (1996). \n                      http:\/\/espace.library.uq.edu.au\/view\/UQ:10768"},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1007\/978-3-319-10181-1_13","volume-title":"Integrated Formal Methods","author":"DL Chaudhari","year":"2014","unstructured":"Chaudhari, D.L., Damani, O.: Automated theorem prover assisted program calculations. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 205\u2013220. Springer, Heidelberg (2014)"},{"key":"15_CR7","unstructured":"Conchon, S., Contejean, E.: The alt-ergo automatic theorem prover (2008). \n                      http:\/\/alt-ergo.lri.fr"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"issue":"8","key":"15_CR9","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"EW Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453\u2013457 (1975)","journal-title":"Commun. ACM"},{"key":"15_CR10","volume-title":"A Discipline of Programming","author":"EW Dijkstra","year":"1997","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice Hall, Englewood Cliffs (1997)"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J-C Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3 \u2014 Where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013)"},{"key":"15_CR12","unstructured":"Franssen, M.: Cocktail: A tool for deriving correct programs. In: Workshop on Automated Reasoning (1999)"},{"key":"15_CR13","volume-title":"The Science of Programming","author":"D Gries","year":"1987","unstructured":"Gries, D.: The Science of Programming, 1st edn. Springer-Verlag New York Inc., Secaucus (1987)","edition":"1"},{"key":"15_CR14","volume-title":"Programming: The Derivation of Algorithms","author":"A Kaldewaij","year":"1990","unstructured":"Kaldewaij, A.: Programming: The Derivation of Algorithms. Prentice-Hall Inc., Upper Saddle River (1990)"},{"key":"15_CR15","volume-title":"Programming from Specifications","author":"C Morgan","year":"1990","unstructured":"Morgan, C.: Programming from Specifications. Prentice-Hall Inc., Englewood Cliffs (1990)"},{"key":"15_CR16","unstructured":"Oliveira, M., Xavier, M., Cavalcanti, A.: Refine and gabriel: support for refinement and tactics. In: Proceedings of the Second International Conference on Software Engineering and Formal Methods, 2004, SEFM 2004, pp. 310\u2013319. IEEE (2004)"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/3-540-45620-1_22","volume-title":"Automated Deduction - CADE-18","author":"C Weidenbach","year":"2002","unstructured":"Weidenbach, C., Brahm, U., Hillenbrand, T., Keen, E., Theobald, C., Topic, D.: SPASS Version 2.0. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 275\u2013279. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Logic-Based Program Synthesis and Transformation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-27436-2_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T20:02:51Z","timestamp":1559332971000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-27436-2_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319274355","9783319274362"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-27436-2_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}