{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T20:30:59Z","timestamp":1725741059631},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642397981"},{"type":"electronic","value":"9783642397998"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39799-8_64","type":"book-chapter","created":{"date-parts":[[2013,7,10]],"date-time":"2013-07-10T19:13:06Z","timestamp":1373483586000},"page":"896-911","source":"Crossref","is-referenced-by-count":9,"title":["Program Repair without Regret"],"prefix":"10.1007","author":[{"given":"Christian","family":"von Essen","sequence":"first","affiliation":[]},{"given":"Barbara","family":"Jobstmann","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"64_CR1","doi-asserted-by":"crossref","unstructured":"Ball, T., Naik, M., Rajamani, S.K.: From symptom to cause: Localizing errors in counterexample traces. In: POPL 2003, pp. 97\u2013105 (January 2003)","DOI":"10.1145\/640128.604140"},{"issue":"1-2","key":"64_CR2","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/S0004-3702(99)00039-9","volume":"112","author":"F. Buccafurri","year":"1999","unstructured":"Buccafurri, F., Eiter, T., Gottlob, G., Leone, N.: Enhancing model checking in verification by ai techniques. Artif. Intell.\u00a0112(1-2), 57\u2013104 (1999)","journal-title":"Artif. Intell."},{"key":"64_CR3","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1090\/S0002-9947-1969-0280205-0","volume":"138","author":"J.R. B\u00fcchi","year":"1969","unstructured":"B\u00fcchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Transactions of the American Mathematical Society\u00a0138, 295\u2013311 (1969)","journal-title":"Transactions of the American Mathematical Society"},{"key":"64_CR4","first-page":"121","volume-title":"ICSE 2011","author":"S. Chandra","year":"2011","unstructured":"Chandra, S., Torlak, E., Barman, S., Bodik, R.: Angelic debugging. In: ICSE 2011, pp. 121\u2013130. ACM, New York (2011)"},{"issue":"1","key":"64_CR5","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1109\/TCAD.2007.907257","volume":"27","author":"K.H. Chang","year":"2008","unstructured":"Chang, K.H., Markov, I.L., Bertacco, V.: Fixing design errors with counterexamples and resynthesis. IEEE Trans. on CAD\u00a027(1), 184\u2013188 (2008)","journal-title":"IEEE Trans. on CAD"},{"key":"64_CR6","unstructured":"Church, A.: Logic, arithmetic and automata. In: Proc. 1962 Int. Congr. Math. (1963)"},{"key":"64_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 359. Springer, Heidelberg (2002)"},{"key":"64_CR8","doi-asserted-by":"crossref","unstructured":"Clarke, E., Grumberg, O., McMillan, K., Zhao, X.: Efficient generation of counterexamples and witnesses in symbolic model checking. In: DAC (1995)","DOI":"10.21236\/ADA288583"},{"key":"64_CR9","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A.: Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. In: Grumberg, O., Veith, H. (eds.) 25MC Festschrift. LNCS, vol.\u00a05000, pp. 196\u2013215. Springer, Heidelberg (2008)","DOI":"10.1007\/978-3-540-69850-0_12"},{"issue":"3","key":"64_CR10","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1145\/176584.176587","volume":"41","author":"D. Drusinsky","year":"1994","unstructured":"Drusinsky, D., Harel, D.: On the power of bounded concurrency i: Finite automata. J. ACM\u00a041(3), 517\u2013539 (1994)","journal-title":"J. ACM"},{"key":"64_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/11795490_22","volume-title":"Principles of Distributed Systems","author":"A. Ebnenasir","year":"2006","unstructured":"Ebnenasir, A., Kulkarni, S.S., Bonakdarpour, B.: Revising unity programs: Possibilities and limitations. In: Anderson, J.H., Prencipe, G., Wattenhofer, R. (eds.) OPODIS 2005. LNCS, vol.\u00a03974, pp. 275\u2013290. Springer, Heidelberg (2006)"},{"key":"64_CR12","doi-asserted-by":"crossref","unstructured":"Edelkamp, S., Lluch-Lafuente, A., Leue, S.: Trail-directed model checking. ENTCS 5(3) (August 2001); Software Model Checking Workshop 2001","DOI":"10.1016\/S1571-0661(04)00261-0"},{"key":"64_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/978-3-540-70583-3_30","volume-title":"Automata, Languages and Programming","author":"K. Greimel","year":"2008","unstructured":"Greimel, K., Bloem, R., Jobstmann, B., Vardi, M.: Open implication. In: Aceto, L., Damg\u00e5rd, I., Goldberg, L.A., Halld\u00f3rsson, M.M., Ing\u00f3lfsd\u00f3ttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part II. LNCS, vol.\u00a05126, pp. 361\u2013372. Springer, Heidelberg (2008)"},{"key":"64_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/11817963_33","volume-title":"Computer Aided Verification","author":"A. Griesmayer","year":"2006","unstructured":"Griesmayer, A., Bloem, R., Cook, B.: Repair of boolean programs with an application to c. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 358\u2013371. Springer, Heidelberg (2006)"},{"key":"64_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/3-540-44829-2_8","volume-title":"Model Checking Software","author":"A. Groce","year":"2003","unstructured":"Groce, A., Visser, W.: What went wrong: Explaining counterexamples. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 121\u2013135. Springer, Heidelberg (2003)"},{"key":"64_CR16","unstructured":"Janjua, M.U., Mycroft, A.: Automatic correction to safety violations in programs. In: Thread Verification (TV 2006) (2006) (unpublished)"},{"key":"64_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1007\/3-540-46002-0_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H. Jin","year":"2002","unstructured":"Jin, H., Ravi, K., Somenzi, F.: Fate and free will in error traces. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 445\u2013459. Springer, Heidelberg (2002)"},{"key":"64_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/11513988_23","volume-title":"Computer Aided Verification","author":"B. Jobstmann","year":"2005","unstructured":"Jobstmann, B., Griesmayer, A., Bloem, R.: Program repair as a game. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 226\u2013238. Springer, Heidelberg (2005)"},{"issue":"2","key":"64_CR19","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1016\/j.jcss.2011.05.005","volume":"78","author":"B. Jobstmann","year":"2012","unstructured":"Jobstmann, B., Staber, S., Griesmayer, A., Bloem, R.: Finding and fixing faults. J. Comput. Syst. Sci.\u00a078(2), 441\u2013460 (2012)","journal-title":"J. Comput. Syst. Sci."},{"key":"64_CR20","doi-asserted-by":"crossref","unstructured":"Kaiss, D., Skaba, M., Hanna, Z., Khasidashvili, Z.: Industrial strength sat-based alignability algorithm for hardware equivalence verification. In: FMCAD, pp. 20\u201326 (2007)","DOI":"10.1109\/FMCAD.2007.4401978"},{"key":"64_CR21","unstructured":"Khasidashvili, Z., Moondanos, J., Kaiss, D., Hanna, Z.: An enhanced cut-points algorithm in formal equivalence verification. In: HLDVT, pp. 171\u2013176 (2001)"},{"key":"64_CR22","doi-asserted-by":"crossref","unstructured":"Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: POPL, pp. 97\u2013107 (1985)","DOI":"10.1145\/318593.318622"},{"issue":"3","key":"64_CR23","doi-asserted-by":"publisher","first-page":"5","DOI":"10.2168\/LMCS-3(3:5)2007","volume":"3","author":"N. Piterman","year":"2007","unstructured":"Piterman, N.: From nondeterministic buchi and streett automata to deterministic parity automata. Logical Methods in Computer Science\u00a03(3), 5 (2007)","journal-title":"Logical Methods in Computer Science"},{"key":"64_CR24","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS. IEEE Comp. Soc. (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"64_CR25","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"64_CR26","doi-asserted-by":"crossref","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Symposium on Programming, pp. 337\u2013351 (1982)","DOI":"10.1007\/3-540-11494-7_22"},{"key":"64_CR27","first-page":"1","volume":"141","author":"M.O. Rabin","year":"1969","unstructured":"Rabin, M.O.: Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society\u00a0141, 1\u201335 (1969)","journal-title":"Transactions of the American Mathematical Society"},{"key":"64_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-540-24730-2_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Ravi","year":"2004","unstructured":"Ravi, K., Somenzi, F.: Minimal assignments for bounded model checking. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 31\u201345. Springer, Heidelberg (2004)"},{"key":"64_CR29","unstructured":"Renieris, M., Reiss, S.P.: Fault localization with nearest neighbor queries. In: ICASE, Montreal, Canada, pp. 30\u201339 (October 2003)"},{"key":"64_CR30","unstructured":"Rosner, R.: Modular Synthesis of Reactive Systems. PhD thesis, Stanford University (1997)"},{"key":"64_CR31","doi-asserted-by":"crossref","unstructured":"Samanta, R., Deshmukh, J.V., Emerson, E.A.: Automatic generation of local repairs for boolean programs. In: Cimatti, A., Jones, R.B. (eds.) FMCAD, pp. 1\u201310 (2008)","DOI":"10.1109\/FMCAD.2008.ECP.31"},{"key":"64_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-00596-1_13","volume-title":"Foundations of Software Science and Computational Structures","author":"S. Schewe","year":"2009","unstructured":"Schewe, S.: Tighter bounds for the determinisation of b\u00fcchi automata. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol.\u00a05504, pp. 167\u2013181. Springer, Heidelberg (2009)"},{"key":"64_CR33","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Rabbah, R.M., Bod\u00edk, R., Ebcioglu, K.: Programming by sketching for bit-streaming programs. In: PLDI, pp. 281\u2013294 (2005)","DOI":"10.1145\/1064978.1065045"},{"key":"64_CR34","doi-asserted-by":"crossref","unstructured":"Vechev, M.T., Yahav, E., Yorsh, G.: Abstraction-guided synthesis of synchronization. In: POPL, pp. 327\u2013338 (2010)","DOI":"10.1145\/1707801.1706338"},{"key":"64_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/978-3-642-00768-2_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Vechev","year":"2009","unstructured":"Vechev, M., Yahav, E., Yorsh, G.: Inferring synchronization under limited observability. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 139\u2013154. Springer, Heidelberg (2009)"},{"key":"64_CR36","doi-asserted-by":"crossref","unstructured":"Wolper, P., Vardi, M.Y., Sistla, A.P.: Reasoning about infinite computation paths (extended abstract). In: FOCS, pp. 185\u2013194. IEEE (1983)","DOI":"10.1109\/SFCS.1983.51"},{"issue":"2","key":"64_CR37","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1109\/32.988498","volume":"28","author":"A. Zeller","year":"2002","unstructured":"Zeller, A., Hildebrandt, R.: Simplifying and isolating failure-inducing input. IEEE Transactions on Software Engineering\u00a028(2), 183\u2013200 (2002)","journal-title":"IEEE Transactions on Software Engineering"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39799-8_64","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T14:40:09Z","timestamp":1557931209000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39799-8_64"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642397981","9783642397998"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39799-8_64","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}