{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,25]],"date-time":"2025-04-25T12:27:37Z","timestamp":1745584057341},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642327582"},{"type":"electronic","value":"9783642327599"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-32759-9_27","type":"book-chapter","created":{"date-parts":[[2012,8,21]],"date-time":"2012-08-21T10:12:30Z","timestamp":1345543950000},"page":"308-325","source":"Crossref","is-referenced-by-count":4,"title":["Theory and Techniques for Synthesizing Efficient Breadth-First Search Algorithms"],"prefix":"10.1007","author":[{"given":"Srinivas","family":"Nedunuri","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Douglas R.","family":"Smith","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"William R.","family":"Cook","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"27_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/3-540-57499-9_16","volume-title":"Formal Program Development","author":"R.S. Bird","year":"1993","unstructured":"Bird, R.S., De Moor, O.: From Dynamic Programming to Greedy Algorithms. In: M\u00f6ller, B., Schuman, S., Partsch, H. (eds.) Formal Program Development. LNCS, vol.\u00a0755, pp. 43\u201361. Springer, Heidelberg (1993)"},{"key":"27_CR2","doi-asserted-by":"crossref","unstructured":"Bj\u00f6rner, A., Ziegler, G.M.: Introduction to greedoids. In: White, N. (ed.) Matroid Applications. Cambridge University Press (1992)","DOI":"10.1017\/CBO9780511662041.009"},{"key":"27_CR3","unstructured":"Cormen, T., Leiserson, C., Rivest, R., Stein, C.: Introduction to Algorithms, 2nd edn. MIT Press (2001)"},{"issue":"1-3","key":"27_CR4","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/j.scico.2003.09.001","volume":"49","author":"S.A. Curtis","year":"2003","unstructured":"Curtis, S.A.: The classification of greedy algorithms. Sci. Comput. Program.\u00a049(1-3), 125\u2013157 (2003)","journal-title":"Sci. Comput. Program."},{"key":"27_CR5","unstructured":"Dechter, R.: Constraint Processing. Morgan Kauffman (2003)"},{"key":"27_CR6","unstructured":"Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design patterns: elements of reusable object-oriented software. Addison-Wesley Professional (1995)"},{"key":"27_CR7","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthesis of loop-free programs. In: PLDI, pp. 62\u201373 (2011)","DOI":"10.1145\/1993316.1993506"},{"issue":"2","key":"27_CR8","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1145\/322003.322010","volume":"24","author":"T. Ibaraki","year":"1977","unstructured":"Ibaraki, T.: The power of dominance relations in branch-and-bound algorithms. J. ACM\u00a024(2), 264\u2013279 (1977)","journal-title":"J. ACM"},{"key":"27_CR9","doi-asserted-by":"crossref","unstructured":"Itzhaky, S., Gulwani, S., Immerman, N., Sagiv, M.: A simple inductive synthesis methodology and its applications. In: OOPSLA, pp. 36\u201346 (2010)","DOI":"10.1145\/1932682.1869463"},{"key":"27_CR10","doi-asserted-by":"crossref","unstructured":"Kreitz, C.: Program synthesis. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction \u2013 A Basis for Applications, vol.\u00a0III, ch. III.2.5, pp. 105\u2013134. Kluwer (1998)","DOI":"10.1007\/978-94-017-0437-3_5"},{"key":"27_CR11","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":"27_CR12","doi-asserted-by":"crossref","unstructured":"Nedunuri, S., Cook, W.R.: Synthesis of fast programs for maximum segment sum problems. In: Intl. Conf. on Generative Prog. and Component Engineering (GPCE) (October 2009)","DOI":"10.1145\/1621607.1621626"},{"key":"27_CR13","doi-asserted-by":"crossref","unstructured":"Nedunuri, S.: Theory and Techniques for Synthesizing Efficient Breadth-First Search Algorithms. PhD thesis, Univ. of Texas at Austin (2012)","DOI":"10.1007\/978-3-642-32759-9_27"},{"key":"27_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/978-3-642-14808-8_24","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2010","author":"S. Nedunuri","year":"2010","unstructured":"Nedunuri, S., Smith, D.R., Cook, W.R.: A Class of Greedy Algorithms and Its Relation to Greedoids. In: Cavalcanti, A., Deharbe, D., Gaudel, M.-C., Woodcock, J. (eds.) ICTAC 2010. LNCS, vol.\u00a06255, pp. 352\u2013366. Springer, Heidelberg (2010)"},{"key":"27_CR15","unstructured":"Nedunuri, S., Smith, D.R., Cook, W.R.: Theory and techniques for synthesizing graph algorithms using breadth-first search. In: 1st Workshop on Synthesis (SYNT) in Computer Aided Verification, CAV (to appear, 2012)"},{"key":"27_CR16","doi-asserted-by":"crossref","unstructured":"Pu, Y., Bod\u00edk, R., Srivastava, S.: Synthesis of first-order dynamic programming algorithms. In: OOPSLA, pp. 83\u201398 (2011)","DOI":"10.1145\/2076021.2048076"},{"key":"27_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-642-13321-3_20","volume-title":"Mathematics of Program Construction","author":"D. Pavlovic","year":"2010","unstructured":"Pavlovic, D., Pepper, P., Smith, D.R.: Formal Derivation of Concurrent Garbage Collectors. In: Bolduc, C., Desharnais, J., Ktari, B. (eds.) MPC 2010. LNCS, vol.\u00a06120, pp. 353\u2013376. Springer, Heidelberg (2010)"},{"key":"27_CR18","unstructured":"Specware, http:\/\/www.specware.org"},{"key":"27_CR19","doi-asserted-by":"crossref","unstructured":"Srivastava, S., Gulwani, S., Foster, J.S.: From program verification to program synthesis. In: POPL, pp. 313\u2013326 (2010)","DOI":"10.1145\/1707801.1706337"},{"key":"27_CR20","doi-asserted-by":"crossref","unstructured":"Sasano, I., Hu, Z., Takeichi, M.: Make it practical: A generic linear-time algorithm for solving maximum-weightsum problems. In: Intl. Conf. Functional Prog. (ICFP) (2000)","DOI":"10.1145\/351240.351254"},{"key":"27_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-44806-3_5","volume-title":"Semantics, Applications, and Implementation of Program Generation","author":"I. Sasano","year":"2001","unstructured":"Sasano, I., Hu, Z.: Generation of Efficient Programs for Solving Maximum Multi-marking Problems. In: Taha, W. (ed.) SAIG 2001. LNCS, vol.\u00a02196, pp. 72\u201391. Springer, Heidelberg (2001)"},{"key":"27_CR22","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Tancau, L., Bodik, R., Seshia, S., Saraswat, V.: Combinatorial sketching for finite programs. In: Proc. of the 12th Intl. Conf. on Architectural Support for Prog. Lang. and Operating Systems (ASPLOS), pp. 404\u2013415 (2006)","DOI":"10.1145\/1168857.1168907"},{"key":"27_CR23","unstructured":"Smith, D.R.: Structure and design of global search algorithms. Tech. Rep. Kes. U.87.12, Kestrel Institute (1988)"},{"issue":"9","key":"27_CR24","doi-asserted-by":"crossref","first-page":"1024","DOI":"10.1109\/32.58788","volume":"16","author":"D.R. Smith","year":"1990","unstructured":"Smith, D.R.: Kids: A semi-automatic program development system. IEEE Trans. on Soft. Eng., Spec. Issue on Formal Methods\u00a016(9), 1024\u20131043 (1990)","journal-title":"IEEE Trans. on Soft. Eng., Spec. Issue on Formal Methods"},{"key":"27_CR25","unstructured":"Smith, D.R.: Global search theory revisited. Unpublished (December 2010)"},{"key":"27_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"562","DOI":"10.1007\/11560647_37","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2005","author":"I. Sasano","year":"2005","unstructured":"Sasano, I., Ogawa, M., Hu, Z.: Maximum Marking Problems with Accumulative Weight Functions. In: Van Hung, D., Wirsing, M. (eds.) ICTAC 2005. LNCS, vol.\u00a03722, pp. 562\u2013578. Springer, Heidelberg (2005)"},{"key":"27_CR27","unstructured":"Smith, D.R., Parra, E.A., Westfold, S.J.: Synthesis of high-performance transportation schedulers. Technical report, Kestrel Institute (1995)"},{"key":"27_CR28","unstructured":"Smith, D.R., Westfold, S.: Synthesis of propositional satisfiability solvers. Final proj. report, Kestrel Institute (2008)"},{"key":"27_CR29","doi-asserted-by":"crossref","unstructured":"Vechev, M., Yahav, E.: Deriving linearizable fine-grained concurrent objects. In: PLDI 2008, pp. 125\u2013135 (2008)","DOI":"10.1145\/1375581.1375598"},{"key":"27_CR30","doi-asserted-by":"crossref","unstructured":"Vechev, M., Yahav, E., Yorsh, G.: Abstraction-guided synthesis of synchronization. In: POPL 2010, pp. 327\u2013338 (2010)","DOI":"10.1145\/1707801.1706338"}],"container-title":["Lecture Notes in Computer Science","FM 2012: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-32759-9_27.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T12:14:54Z","timestamp":1620130494000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-32759-9_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642327582","9783642327599"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-32759-9_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}