{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,26]],"date-time":"2025-04-26T14:26:47Z","timestamp":1745677607805},"reference-count":48,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2015,2,24]],"date-time":"2015-02-24T00:00:00Z","timestamp":1424736000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2015,8]]},"DOI":"10.1007\/s10703-015-0223-6","type":"journal-article","created":{"date-parts":[[2015,2,23]],"date-time":"2015-02-23T13:52:23Z","timestamp":1424699543000},"page":"26-50","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["Program repair without regret"],"prefix":"10.1007","volume":"47","author":[{"given":"Christian","family":"von Essen","sequence":"first","affiliation":[]},{"given":"Barbara","family":"Jobstmann","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,2,24]]},"reference":[{"key":"223_CR1","doi-asserted-by":"crossref","unstructured":"Alur R, Bod\u00edk R, Juniwal G, Martin MMK, Raghothaman M, Seshia SA, Singh R, Solar-Lezama A, Torlak E, Udupa A (2013) Syntax-guided synthesis. Paper presented at the conference on FMCAD, IEEE, New York, pp 1\u201317, Oct 2013","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"223_CR2","first-page":"169","volume-title":"TACAS","author":"A Bohy","year":"2013","unstructured":"Bohy A, Bruy\u00e8re V, Filiot E, Raskin J-F (2013) Synthesis from LTL specifications with mean-payoff objectives. In: Piterman N, Smolka SA (eds) TACAS, vol 7795. Springer, Heidelberg, pp 169\u2013184"},{"issue":"1\u20132","key":"223_CR3","doi-asserted-by":"crossref","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 (1999) Enhancing model checking in verification by ai techniques. Artif Intell 112(1\u20132):57\u2013104","journal-title":"Artif Intell"},{"issue":"1","key":"223_CR4","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1145\/1462187.1462192","volume":"4","author":"B Bonakdarpour","year":"2009","unstructured":"Bonakdarpour B, Ebnenasir A, Kulkarni SS (2009) Complexity results in revising unity programs. TAAS 4(1):5","journal-title":"TAAS"},{"key":"223_CR5","doi-asserted-by":"crossref","unstructured":"Bonakdarpour B, Hajisheykhi R, Kulkarni SS (2014) Knowledge-based automated repair of authentication protocols. In: Jones CB, Pihlajasaari P, Sun J (eds) 19th International symposium on FM: lecture notes in computer science. vol 8442. Springer, pp 132\u2013147, 2014","DOI":"10.1007\/978-3-319-06410-9_10"},{"issue":"5\u20136","key":"223_CR6","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1007\/s10009-013-0287-9","volume":"15","author":"R Bod\u00edk","year":"2013","unstructured":"Bod\u00edk R, Jobstmann B (2013) Algorithmic program synthesis: introduction. STTT 15(5\u20136):397\u2013411","journal-title":"STTT"},{"issue":"1","key":"223_CR7","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/s00446-011-0139-3","volume":"25","author":"B Bonakdarpour","year":"2012","unstructured":"Bonakdarpour B, Kulkarni SS, Abujarad F (2012) Symbolic synthesis of masking fault-tolerant distributed programs. Distrib Comput 25(1):83\u2013108","journal-title":"Distrib Comput"},{"key":"223_CR8","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1090\/S0002-9947-1969-0280205-0","volume":"138","author":"JR B\u00fcchi","year":"1969","unstructured":"B\u00fcchi JR, Landweber LH (1969) Solving sequential conditions by finite-state strategies. Trans Am Math Soc 138:295\u2013311","journal-title":"Trans Am Math Soc"},{"key":"223_CR9","doi-asserted-by":"crossref","unstructured":"Ball T, Naik M, Rajamani SK (2003) From symptom to cause: localizing errors in counterexample traces. In: Aiken A, Morrisett G (eds) In: Conference on POPL, ACM, New Orleans, pp 97\u2013105, Jully 2003","DOI":"10.1145\/604131.604140"},{"key":"223_CR10","unstructured":"\u010cer\u0144y P, Henzinger TA, Radhakrishna A (2010) Simulation distances. In: Proceedings of the 21st international conference on concurrency theory, CONCUR\u201910. Springer, Berlin, pp 253\u2013268"},{"key":"223_CR11","unstructured":"Cimatti A, Clarke E, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A (2002) NuSMV Version 2: an opensource tool for symbolic model checking. In: 14th International conference on CAV, Springer, New York, July 2002"},{"key":"223_CR12","first-page":"52","volume-title":"Logic of programs","author":"EM Clarke","year":"1981","unstructured":"Clarke EM, Emerson EA (1981) Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen D (ed) Logic of programs, vol 131. Springer, New York, pp 52\u201371"},{"key":"223_CR13","doi-asserted-by":"crossref","unstructured":"Clarke EM, Grumberg O, McMillan KL, Zhao X (1995) Efficient generation of counterexamples and witnesses in symbolic model checking. In proceedings of the 32nd annual ACM\/IEEE Design Automation Conference, ACM, New York, pp 427\u2013432, Jan 1995","DOI":"10.1145\/217474.217565"},{"key":"223_CR14","doi-asserted-by":"crossref","unstructured":"Chatterjee K, Henzinger TA, Jurdzinski M (2005) Mean-payoff parity games. In proceedings of the 20th annual IEEE symposium on LICS, IEEE Computer Society, New York, pp 178\u2013187, June 2005","DOI":"10.1109\/LICS.2005.26"},{"key":"223_CR15","unstructured":"Church A (1963) In: Clarke E, Emerson EA, Sistla AP (eds) Proceedings of the 5th international congress of mathematicians, pp 23\u201325, Aug 1962"},{"issue":"1","key":"223_CR16","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1109\/TCAD.2007.907257","volume":"27","author":"K-H Chang","year":"2008","unstructured":"Chang K-H, Markov IL, Bertacco V (2008) Fixing design errors with counterexamples and resynthesis. IEEE Trans CAD Integr Circuits Syst 27(1):184\u2013188","journal-title":"IEEE Trans CAD Integr Circuits Syst"},{"key":"223_CR17","doi-asserted-by":"crossref","unstructured":"Chandra S, Torlak E, Barman S, ZBodik R (2011) Angelic debugging. In: 33rd International conference on software engineering (ICSE), ACM, New York, pp 121\u2013130, May 2011","DOI":"10.1145\/1985793.1985811"},{"issue":"3","key":"223_CR18","doi-asserted-by":"crossref","first-page":"517","DOI":"10.1145\/176584.176587","volume":"41","author":"D Drusinsky","year":"1994","unstructured":"Drusinsky D, Harel D (1994) On the power of bounded concurrency i: finite automata. J ACM 41(3):517\u2013539","journal-title":"J ACM"},{"key":"223_CR19","unstructured":"Ebnenasir A, Kulkarni SS, Bonakdarpour B (2005) Revising unity programs: possibilities and limitations. In: OPODIS. Springer, Heidelberg, pp 275\u2013290, 2005"},{"issue":"3","key":"223_CR20","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1016\/S1571-0661(04)00261-0","volume":"55","author":"S Edelkamp","year":"2001","unstructured":"Edelkamp S, Lluch-Lafuente A, Leue S (2001) Trail-directed model checking. Electron Notes Theor Comput Sci 55(3):343\u2013356","journal-title":"Electron Notes Theor Comput Sci"},{"key":"223_CR21","doi-asserted-by":"crossref","unstructured":"Griesmayer A, Bloem R, Cook B (2006) Repair of boolean programs with an application to c. In: Ball T, Jones R (eds) CAV, volume 4144 of LNCS, Springer, Heidelberg, pp 358\u2013371, 2006","DOI":"10.1007\/11817963_33"},{"key":"223_CR22","doi-asserted-by":"crossref","unstructured":"Greimel K, Bloem R, Jobstmann B, Vardi M (2008) Open implication. In: ICALP, LNCS 5126, Springer, Heidelberg, pp 361\u2013372, 2008","DOI":"10.1007\/978-3-540-70583-3_30"},{"key":"223_CR23","first-page":"121","volume-title":"SPIN","author":"A Groce","year":"2003","unstructured":"Groce A, Visser W (2003) What went wrong: explaining counterexamples. In: Ball T, Rajamani SK (eds) SPIN. Springer, New York, pp 121\u2013135"},{"key":"223_CR24","first-page":"226","volume-title":"CAV","author":"B Jobstmann","year":"2005","unstructured":"Jobstmann B, Griesmayer A, Bloem R (2005) Program repair as a game. In: Ball T, Jones RB (eds) CAV. Springer, Heidelberg, pp 226\u2013238"},{"key":"223_CR25","unstructured":"Janjua MU, Mycroft A (2006) Automatic correction to safety violations in programs. Thread Verification (TV\u201906). Unpublished"},{"issue":"2","key":"223_CR26","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1007\/s10009-004-0146-9","volume":"6","author":"HS Jin","year":"2004","unstructured":"Jin HS, Ravi K, Somenzi F (2004) Fate and free will in error traces. STTT 6(2):102\u2013116","journal-title":"STTT"},{"issue":"2","key":"223_CR27","doi-asserted-by":"crossref","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 (2012) Finding and fixing faults. J Comput Syst Sci 78(2):441\u2013460","journal-title":"J Comput Syst Sci"},{"key":"223_CR28","doi-asserted-by":"crossref","unstructured":"Khasidashvili Z, Moondanos J, Kaiss D, Hanna Z (2001) An enhanced cut-points algorithm in formal equivalence verification. In: Sixth IEEE international proceedings of the HLDVT, pp 171\u2013176, 2001","DOI":"10.1109\/HLDVT.2001.972825"},{"key":"223_CR29","doi-asserted-by":"crossref","unstructured":"Kaiss D, Skaba M, Hanna Z, Khasidashvili Z (2007) Industrial strength sat-based alignability algorithm for hardware equivalence verification. In: Proceedings of the FMCAD, IEEE, pp 20\u201326, 2007","DOI":"10.1109\/FAMCAD.2007.37"},{"key":"223_CR30","doi-asserted-by":"crossref","unstructured":"Lichtenstein O, Pnueli A (1985) Checking that finite state concurrent programs satisfy their linear specification. In: Proceedings of the POPL, ACM, New York, pp 97\u2013107, Jan 1985","DOI":"10.1145\/318593.318622"},{"key":"223_CR31","doi-asserted-by":"crossref","unstructured":"Piterman N (2006) From nondeterministic buchi and streett automata to deterministic parity automata. In: 21st annual IEEE symposium on LICS, IEEE, pp 255\u2013264, 2006","DOI":"10.1109\/LICS.2006.28"},{"issue":"3","key":"223_CR32","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-3(3:5)2007","volume":"3","author":"N Piterman","year":"2007","unstructured":"Piterman N (2007) From nondeterministic b\u00fcchi and streett automata to deterministic parity automata. Log Methods Comput Sci 3(3):1\u201321","journal-title":"Log Methods Comput Sci"},{"key":"223_CR33","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: IEEE Symposium on FOCS, pp 46\u201357, 1977","DOI":"10.1109\/SFCS.1977.32"},{"key":"223_CR34","doi-asserted-by":"crossref","unstructured":"Pnueli A, Rosner R (1989) On the synthesis of a reactive module. In: proceedings of the 16th ACM Symposium on POPL, ACM, pp 179\u2013190, Jan 1989","DOI":"10.1145\/75277.75293"},{"key":"223_CR35","doi-asserted-by":"crossref","unstructured":"Puterman ML (1994) Markov decision processes: discrete stochastic dynamic programming. Wiley, New York","DOI":"10.1002\/9780470316887"},{"key":"223_CR36","doi-asserted-by":"crossref","unstructured":"Queille J-P, Sifakis J (1982) Specification and verification of concurrent systems in CESAR. In: 5th international symposium on programming, pp 337\u2013351, 1982","DOI":"10.1007\/3-540-11494-7_22"},{"key":"223_CR37","first-page":"1","volume":"141","author":"MO Rabin","year":"1969","unstructured":"Rabin MO (1969) Decidability of second-order theories and automata on infinite trees. Trans Am Math Soc 141:1\u201335","journal-title":"Trans Am Math Soc"},{"key":"223_CR38","unstructured":"Rosner R (1997) Modular synthesis of reactive systems. PhD thesis, Stanford University"},{"key":"223_CR39","doi-asserted-by":"crossref","unstructured":"Renieris M, Reiss SP (2003) Fault localization with nearest neighbor queries. In: Proceedings of the 18th IEEE international conference on ASE, IEEE, pp 30\u201339, 2003","DOI":"10.1109\/ASE.2003.1240292"},{"key":"223_CR40","doi-asserted-by":"crossref","unstructured":"Ravi K, Somenzi F (2004) Minimal assignments for bounded model checking. In: Proceedings of TACAS, Springer, Heidelberg, pp 31\u201345, Apr 2004","DOI":"10.1007\/978-3-540-24730-2_3"},{"key":"223_CR41","doi-asserted-by":"crossref","unstructured":"Safra S (1988) On the complexity of omega-automata. In: Proceedings of the FOCS, IEEE, pp 319\u2013327, Oct 1988","DOI":"10.1109\/SFCS.1988.21948"},{"key":"223_CR42","doi-asserted-by":"crossref","unstructured":"Schewe S (2009) Tighter bounds for the determinisation of b\u00fcchi automata. In: 12th international conference on FOSSACS, Springer, New York, pp 167\u2013181, 2009","DOI":"10.1007\/978-3-642-00596-1_13"},{"key":"223_CR43","doi-asserted-by":"crossref","unstructured":"Samanta R, Deshmukh JV, Emerson EA (2008) Automatic generation of local repairs for boolean programs. In: FMCAD, Springer, Heidelberg, pp 1\u201310, 2008","DOI":"10.1109\/FMCAD.2008.ECP.31"},{"key":"223_CR44","doi-asserted-by":"crossref","unstructured":"von Essen C, Jobstmann B (2013) Program repair without regret. In: Proceedings of CAV, Springer, Berlin, Heidelberg, pp 896\u2013911, 2013","DOI":"10.1007\/978-3-642-39799-8_64"},{"key":"223_CR45","doi-asserted-by":"crossref","unstructured":"Vechev M, Yahav E, Yorsh G (2009) Inferring synchronization under limited observability. In: TACAS\u201909, vol. 5505 of LNCS, Springer, New York, pp 139\u2013154, 2009","DOI":"10.1007\/978-3-642-00768-2_13"},{"key":"223_CR46","doi-asserted-by":"crossref","unstructured":"Vechev MT, Yahav E, Yorsh G (2010) Abstraction-guided synthesis of synchronization. In: Proceedings of POPL, pp 327\u2013338, 2010","DOI":"10.1145\/1706299.1706338"},{"key":"223_CR47","unstructured":"Wolper P, Vardi MY, Sistla AP (1983) Reasoning about infinite computation paths (extended abstract). In: Proceedings of the FOCS, Tucson, pp 185\u2013194, 1983"},{"issue":"2","key":"223_CR48","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1109\/32.988498","volume":"28","author":"A Zeller","year":"2002","unstructured":"Zeller A, Hildebrandt R (2002) Simplifying and isolating failure-inducing input. IEEE Trans Softw Eng 28(2):183\u2013200","journal-title":"IEEE Trans Softw Eng"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-015-0223-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-015-0223-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-015-0223-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,21]],"date-time":"2019-08-21T04:47:30Z","timestamp":1566362850000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-015-0223-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,2,24]]},"references-count":48,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,8]]}},"alternative-id":["223"],"URL":"https:\/\/doi.org\/10.1007\/s10703-015-0223-6","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,2,24]]}}}