{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:41:15Z","timestamp":1751661675695,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319101804"},{"type":"electronic","value":"9783319101811"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-10181-1_13","type":"book-chapter","created":{"date-parts":[[2014,8,29]],"date-time":"2014-08-29T14:28:38Z","timestamp":1409322518000},"page":"205-220","source":"Crossref","is-referenced-by-count":5,"title":["Automated Theorem Prover Assisted Program Calculations"],"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","reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Bodik, R., Juniwal, G., Martin, M.M.K., Raghothaman, M., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. In: Proceedings of the IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD) (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"issue":"5-6","key":"13_CR2","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/BF01211456","volume":"9","author":"R. Back","year":"1997","unstructured":"Back, R., Grundy, J., Von Wright, J.: Structured calculational proof. Formal Aspects of Computing\u00a09(5-6), 469\u2013483 (1997)","journal-title":"Formal Aspects of Computing"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Back, R.J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science. Springer, Berlin (1998)","DOI":"10.1007\/978-1-4612-1674-2_1"},{"key":"13_CR4","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":"C. Barrett","year":"2007","unstructured":"Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 298\u2013302. Springer, Heidelberg (2007)"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","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.\u00a01125, pp. 93\u2013108. Springer, Heidelberg (1996)"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Carrington, D., Hayes, I., Nickson, R., Watson, G.N., Welsh, J.: A tool for developing correct programs by refinement. Tech. rep. (1996), \n                        http:\/\/espace.library.uq.edu.au\/view\/UQ:10768","DOI":"10.14236\/ewic\/RW1996.3"},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E. Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 23\u201342. Springer, Heidelberg (2009)"},{"key":"13_CR8","unstructured":"Conchon, S., Contejean, E.: The alt-ergo automatic theorem prover (2008), \n                        http:\/\/alt-ergo.lri.fr"},{"key":"13_CR9","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. De Moura","year":"2008","unstructured":"De Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"issue":"8","key":"13_CR10","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E.W. Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM\u00a018(8), 453\u2013457 (1975)","journal-title":"Commun. ACM"},{"key":"13_CR11","unstructured":"Dijkstra, E.W., Feijen, W.H.: A Method of Programming. Addison-Wesley Longman Publishing Co., Inc., Boston (1988)"},{"key":"13_CR12","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice Hall, NJ (1997)"},{"key":"13_CR13","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.) Programming Languages and Systems. LNCS, vol.\u00a07792, pp. 125\u2013128. Springer, Heidelberg (2013)"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Grundy, J.: A window inference tool for refinement. In: 5th Refinement Workshop, pp. 230\u2013254. Springer (1992)","DOI":"10.1007\/978-1-4471-3550-0_12"},{"key":"13_CR15","unstructured":"Grundy, J.: A Method of Program Refinement. Ph.D. thesis, University of Cambridge Computer Laboratory, Cambridge, England (1993)"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthesis of loop-free programs. In: Hall, M.W., Padua, D.A. (eds.) Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4-8, pp. 62\u201373. ACM (2011)","DOI":"10.1145\/1993498.1993506"},{"key":"13_CR17","unstructured":"Jacobs, B., Piessens, F.: The VeriFast program verifier. Technical Report CW-520, Dept. of Computer Science, Katholieke Universiteit Leuven (2008), \n                        http:\/\/www.cs.kuleuven.be\/~bartj\/verifast\/verifast.pdf"},{"key":"13_CR18","unstructured":"Kaldewaij, A.: Programming: The Derivation of Algorithms. Prentice-Hall, Inc., NJ, USA (1990)"},{"key":"13_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"K.R.M. Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol.\u00a06355, pp. 348\u2013370. Springer, Heidelberg (2010)"},{"key":"13_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/978-3-642-54108-7_9","volume-title":"Verified Software: Theories, Tools, Experiments","author":"K.R.M. Leino","year":"2014","unstructured":"Leino, K.R.M., Polikarpova, N.: Verified calculations. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol.\u00a08164, pp. 170\u2013190. Springer, Heidelberg (2014)"},{"key":"13_CR21","unstructured":"Morgan, C.: Programming from Specifications. Prentice-Hall, Inc. (1990)"},{"issue":"1","key":"13_CR22","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1093\/logcom\/3.1.47","volume":"3","author":"P.J. Robinson","year":"1993","unstructured":"Robinson, P.J., Staples, J.: Formalizing a hierarchical structure of practical mathematical reasoning. Journal of Logic and Computation\u00a03(1), 47\u201361 (1993)","journal-title":"Journal of Logic and Computation"},{"issue":"5","key":"13_CR23","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1145\/1168919.1168907","volume":"34","author":"A. Solar-Lezama","year":"2006","unstructured":"Solar-Lezama, A., Tancau, L., Bodik, R., Seshia, S., Saraswat, V.: Combinatorial sketching for finite programs. ACM SIGARCH Computer Architecture News\u00a034(5), 404\u2013415 (2006)","journal-title":"ACM SIGARCH Computer Architecture News"},{"key":"13_CR24","doi-asserted-by":"crossref","unstructured":"Srivastava, S., Gulwani, S., Foster, J.S.: From program verification to program synthesis. In: POPL 2010, New York, NY, USA, pp. 313\u2013326 (2010)","DOI":"10.1145\/1707801.1706337"},{"key":"13_CR25","series-title":"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.\u00a02392, pp. 275\u2013279. Springer, Heidelberg (2002)"},{"key":"13_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/BFb0055127","volume-title":"Theorem Proving in Higher Order Logics","author":"J. von Wright","year":"1998","unstructured":"von Wright, J.: Extending window inference. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol.\u00a01479, pp. 17\u201332. Springer, Heidelberg (1998)"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10181-1_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,28]],"date-time":"2023-01-28T08:26:53Z","timestamp":1674894413000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-10181-1_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319101804","9783319101811"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10181-1_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}