{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T16:40:18Z","timestamp":1768322418821,"version":"3.49.0"},"publisher-location":"Cham","reference-count":57,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031656323","type":"print"},{"value":"9783031656330","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,26]],"date-time":"2024-07-26T00:00:00Z","timestamp":1721952000000},"content-version":"vor","delay-in-days":207,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We study the problem of automatically repairing infinite-state software programs w.r.t.\u00a0temporal hyperproperties. As a first step, we present a repair approach for the temporal logic HyperLTL based on symbolic execution, constraint generation, and syntax-guided synthesis of repair expression (SyGuS). To improve the repair quality, we introduce the notation of a <jats:italic>transparent<\/jats:italic> repair that aims to find a patch that is as close as possible to the original program. As a practical realization, we develop an <jats:italic>iterative<\/jats:italic> repair approach. Here, we search for a sequence of repairs that are closer and closer to the original program\u2019s behavior. We implement our method in a prototype and report on encouraging experimental results using off-the-shelf SyGuS solvers.<\/jats:p>","DOI":"10.1007\/978-3-031-65633-0_1","type":"book-chapter","created":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:03:08Z","timestamp":1721890988000},"page":"3-26","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Syntax-Guided Automated Program Repair for\u00a0Hyperproperties"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6234-5651","authenticated-orcid":false,"given":"Raven","family":"Beutner","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6277-2765","authenticated-orcid":false,"given":"Tzu-Han","family":"Hsu","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1800-5419","authenticated-orcid":false,"given":"Borzoo","family":"Bonakdarpour","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4280-8441","authenticated-orcid":false,"given":"Bernd","family":"Finkbeiner","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,26]]},"reference":[{"key":"1_CR1","doi-asserted-by":"publisher","unstructured":"Agrawal, S., Bonakdarpour, B.: Runtime verification of k-safety hyperproperties in HyperLTL. In: Computer Security Foundations Symposium, CSF 2016 (2016). https:\/\/doi.org\/10.1109\/CSF.2016.24","DOI":"10.1109\/CSF.2016.24"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., et al.: Syntax-guided synthesis. In: Formal Methods in Computer-Aided Design, FMCAD 2013 (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"1_CR3","doi-asserted-by":"publisher","unstructured":"Alur, R., Radhakrishna, A., Udupa, A.: Scaling enumerative program synthesis via divide and conquer. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2017 (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_18","DOI":"10.1007\/978-3-662-54577-5_18"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-030-99524-9_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Barbosa","year":"2022","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: TACAS 2022. LNCS, vol. 13243, pp. 415\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24"},{"key":"1_CR5","doi-asserted-by":"publisher","unstructured":"Baumeister, J., Coenen, N., Bonakdarpour, B., Finkbeiner, B., S\u00e1nchez, C.: A temporal logic for asynchronous hyperproperties. In: International Conference on Computer Aided Verification, CAV 2021 (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_33","DOI":"10.1007\/978-3-030-81685-8_33"},{"key":"1_CR6","doi-asserted-by":"publisher","unstructured":"Beutner, R., Finkbeiner, B.: Prophecy variables for hyperproperty verification. In: Computer Security Foundations Symposium, CSF 2022 (2022). https:\/\/doi.org\/10.1109\/CSF54842.2022.9919658","DOI":"10.1109\/CSF54842.2022.9919658"},{"key":"1_CR7","doi-asserted-by":"publisher","unstructured":"Beutner, R., Finkbeiner, B.: Software verification of hyperproperties beyond k-safety. In: International Conference on Computer Aided Verification, CAV 2022 (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_17","DOI":"10.1007\/978-3-031-13185-1_17"},{"key":"1_CR8","doi-asserted-by":"publisher","unstructured":"Beutner, R., Finkbeiner, B.: AutoHyper: explicit-state model checking for HyperLTL. In: Sankaranarayanan, S., Sharygina, N. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2023. LNCS, vol. 13993, pp. 145\u2013163. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_8","DOI":"10.1007\/978-3-031-30823-9_8"},{"key":"1_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/978-3-030-31784-3_25","volume-title":"Automated Technology for Verification and Analysis","author":"B Bonakdarpour","year":"2019","unstructured":"Bonakdarpour, B., Finkbeiner, B.: Program repair for hyperproperties. In: Chen, Y.-F., Cheng, C.-H., Esparza, J. (eds.) ATVA 2019. LNCS, vol. 11781, pp. 423\u2013441. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_25"},{"key":"1_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/978-3-030-03421-4_2","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Verification","author":"B Bonakdarpour","year":"2018","unstructured":"Bonakdarpour, B., Sanchez, C., Schneider, G.: Monitoring hyperproperties by combining static analysis and runtime verification. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 8\u201327. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03421-4_2"},{"key":"1_CR11","doi-asserted-by":"publisher","unstructured":"Bozzelli, L., Peron, A., S\u00e1nchez, C.: Asynchronous extensions of HyperLTL. In: Symposium on Logic in Computer Science, LICS 2021 (2021). https:\/\/doi.org\/10.1109\/LICS52264.2021.9470583","DOI":"10.1109\/LICS52264.2021.9470583"},{"key":"1_CR12","doi-asserted-by":"publisher","unstructured":"Chaudhuri, S., Gulwani, S., Lublinerman, R.: Continuity and robustness of programs. Commun. ACM 55(8) (2012). https:\/\/doi.org\/10.1145\/2240236.2240262","DOI":"10.1145\/2240236.2240262"},{"key":"1_CR13","doi-asserted-by":"publisher","unstructured":"Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., S\u00e1nchez, C.: Temporal logics for hyperproperties. In: International Conference on Principles of Security and Trust, POST 2014 (2014). https:\/\/doi.org\/10.1007\/978-3-642-54792-8_15","DOI":"10.1007\/978-3-642-54792-8_15"},{"key":"1_CR14","doi-asserted-by":"publisher","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. In: Computer Security Foundations Symposium, CSF 2008 (2008). https:\/\/doi.org\/10.1109\/CSF.2008.7","DOI":"10.1109\/CSF.2008.7"},{"key":"1_CR15","doi-asserted-by":"publisher","unstructured":"Coenen, N., Finkbeiner, B., Hahn, C., Hofmann, J., Schillo, Y.: Runtime enforcement of hyperproperties. In: International Symposium on Automated Technology for Verification and Analysis, ATVA 2021 (2021). https:\/\/doi.org\/10.1007\/978-3-030-88885-5_19","DOI":"10.1007\/978-3-030-88885-5_19"},{"key":"1_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-030-25540-4_7","volume-title":"Computer Aided Verification","author":"N Coenen","year":"2019","unstructured":"Coenen, N., Finkbeiner, B., S\u00e1nchez, C., Tentrup, L.: Verifying hyperliveness. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 121\u2013139. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_7"},{"key":"1_CR17","doi-asserted-by":"publisher","unstructured":"Daniel, L., Bardin, S., Rezk, T.: Binsec\/Rel: efficient relational symbolic execution for constant-time at binary-level. In: Symposium on Security and Privacy, SP 2020 (2020). https:\/\/doi.org\/10.1109\/SP40000.2020.00074","DOI":"10.1109\/SP40000.2020.00074"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Daniel, L., Bardin, S., Rezk, T.: Hunting the haunter - efficient relational symbolic execution for Spectre with haunted RelSE. In: Annual Network and Distributed System Security Symposium, NDSS 2021 (2021)","DOI":"10.14722\/ndss.2021.24286"},{"key":"1_CR19","doi-asserted-by":"publisher","DOI":"10.1145\/3632913","author":"Y Ding","year":"2024","unstructured":"Ding, Y., Qiu, X.: Enhanced enumeration techniques for syntax-guided synthesis of bit-vector manipulations. Proc. ACM Program. Lang. (POPL) (2024). https:\/\/doi.org\/10.1145\/3632913","journal-title":"Proc. ACM Program. Lang. (POPL)"},{"key":"1_CR20","doi-asserted-by":"publisher","unstructured":"Duret-Lutz, A., et al.: From spot 2.0 to spot 2.10: what\u2019s new? In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification, CAV 2022. LNCS, vol. 13372, pp. 174\u2013187. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_9","DOI":"10.1007\/978-3-031-13188-2_9"},{"key":"1_CR21","doi-asserted-by":"publisher","unstructured":"Fan, Z., Gao, X., Mirchev, M., Roychoudhury, A., Tan, S.H.: Automated repair of programs from large language models. In: International Conference on Software Engineering, ICSE 2023 (2023). https:\/\/doi.org\/10.1109\/ICSE48619.2023.00128","DOI":"10.1109\/ICSE48619.2023.00128"},{"key":"1_CR22","doi-asserted-by":"publisher","unstructured":"Farina, G.P., Chong, S., Gaboardi, M.: Relational symbolic execution. In: International Symposium on Principles and Practice of Programming Languages, PPDP 2019 (2019). https:\/\/doi.org\/10.1145\/3354166.3354175","DOI":"10.1145\/3354166.3354175"},{"key":"1_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-030-25540-4_11","volume-title":"Computer Aided Verification","author":"A Farzan","year":"2019","unstructured":"Farzan, A., Vandikas, A.: Automated hypersafety verification. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 200\u2013218. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_11"},{"key":"1_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-319-21690-4_3","volume-title":"Computer Aided Verification","author":"B Finkbeiner","year":"2015","unstructured":"Finkbeiner, B., Rabe, M.N., S\u00e1nchez, C.: Algorithms for model checking HyperLTL and HyperCTL$$^*$$. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 30\u201348. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_3"},{"key":"1_CR25","doi-asserted-by":"publisher","unstructured":"Gazzola, L., Micucci, D., Mariani, L.: Automatic software repair: a survey. IEEE Trans. Softw. Eng. 45(1) (2019). https:\/\/doi.org\/10.1109\/TSE.2017.2755013","DOI":"10.1109\/TSE.2017.2755013"},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"Gordon, M.I., Kim, D., Perkins, J.H., Gilham, L., Nguyen, N., Rinard, M.C.: Information flow analysis of android applications in DroidSafe. In: Annual Network and Distributed System Security Symposium, NDSS 2015 (2015)","DOI":"10.14722\/ndss.2015.23089"},{"key":"1_CR27","doi-asserted-by":"publisher","unstructured":"Goues, C.L., Dewey-Vogt, M., Forrest, S., Weimer, W.: A systematic study of automated program repair: fixing 55 out of 105 bugs for \\$8 each. In: International Conference on Software Engineering, ICSE 2012 (2012). https:\/\/doi.org\/10.1109\/ICSE.2012.6227211","DOI":"10.1109\/ICSE.2012.6227211"},{"key":"1_CR28","doi-asserted-by":"publisher","unstructured":"Goues, C.L., Pradel, M., Roychoudhury, A.: Automated program repair. Commun. ACM 62(12) (2019). https:\/\/doi.org\/10.1145\/3318162","DOI":"10.1145\/3318162"},{"key":"1_CR29","doi-asserted-by":"publisher","DOI":"10.1145\/3434319","author":"JO Gutsfeld","year":"2021","unstructured":"Gutsfeld, J.O., M\u00fcller-Olm, M., Ohrem, C.: Automata and fixpoints for asynchronous hyperproperties. Proc. ACM Program. Lang. (POPL) (2021). https:\/\/doi.org\/10.1145\/3434319","journal-title":"Proc. ACM Program. Lang. (POPL)"},{"key":"1_CR30","doi-asserted-by":"publisher","unstructured":"Hamann, T., Herda, M., Mantel, H., Mohr, M., Schneider, D., Tasch, M.: A uniform information-flow security benchmark suite for source code and bytecode. In: Nordic Conference on Secure IT Systems, NordSec 2018 (2018). https:\/\/doi.org\/10.1007\/978-3-030-03638-6_27","DOI":"10.1007\/978-3-030-03638-6_27"},{"key":"1_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/978-3-030-72016-2_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T-H Hsu","year":"2021","unstructured":"Hsu, T.-H., S\u00e1nchez, C., Bonakdarpour, B.: Bounded model checking for hyperproperties. In: TACAS 2021. LNCS, vol. 12651, pp. 94\u2013112. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_6"},{"key":"1_CR32","doi-asserted-by":"publisher","unstructured":"Hsu, T., S\u00e1nchez, C., Sheinvald, S., Bonakdarpour, B.: Efficient loop conditions for bounded model checking hyperproperties. In: Sankaranarayanan, S., Sharygina, N. (eds.) International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2023. LNCS, vol. 13993, pp. 66\u201384. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_4","DOI":"10.1007\/978-3-031-30823-9_4"},{"key":"1_CR33","doi-asserted-by":"publisher","unstructured":"Huang, K., Qiu, X., Shen, P., Wang, Y.: Reconciling enumerative and deductive program synthesis. In: International Conference on Programming Language Design and Implementation, PLDI 2020 (2020). https:\/\/doi.org\/10.1145\/3385412.3386027","DOI":"10.1145\/3385412.3386027"},{"key":"1_CR34","doi-asserted-by":"publisher","unstructured":"Itzhaky, S., Shoham, S., Vizel, Y.: Hyperproperty verification as CHC satisfiability. In: Weirich, S. (eds.) European Symposium on Programming Languages and Systems, ESOP 2024. LNCS, vol. 14577, pp. 212\u2013241. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-57267-8_9","DOI":"10.1007\/978-3-031-57267-8_9"},{"key":"1_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-319-13841-1_6","volume-title":"Information Systems Security","author":"W Khan","year":"2014","unstructured":"Khan, W., Calzavara, S., Bugliesi, M., De Groef, W., Piessens, F.: Client side web session integrity as a non-interference property. In: Prakash, A., Shyamasundar, R. (eds.) ICISS 2014. LNCS, vol. 8880, pp. 89\u2013108. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-13841-1_6"},{"key":"1_CR36","doi-asserted-by":"publisher","unstructured":"Kim, D., Nam, J., Song, J., Kim, S.: Automatic patch generation learned from human-written patches. In: International Conference on Software Engineering, ICSE 2013 (2013). https:\/\/doi.org\/10.1109\/ICSE.2013.6606626","DOI":"10.1109\/ICSE.2013.6606626"},{"key":"1_CR37","doi-asserted-by":"publisher","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7) (1976). https:\/\/doi.org\/10.1145\/360248.360252","DOI":"10.1145\/360248.360252"},{"key":"1_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/3-540-48683-6_17","volume-title":"Computer Aided Verification","author":"O Kupferman","year":"1999","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 172\u2013183. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48683-6_17"},{"key":"1_CR39","doi-asserted-by":"publisher","unstructured":"Le, X.D., Chu, D., Lo, D., Goues, C.L., Visser, W.: S3: syntax- and semantic-guided repair synthesis via programming by examples. In: Joint Meeting on Foundations of Software Engineering, ESEC\/FSE 2017 (2017). https:\/\/doi.org\/10.1145\/3106237.3106309","DOI":"10.1145\/3106237.3106309"},{"key":"1_CR40","doi-asserted-by":"publisher","unstructured":"Liu, K., Koyuncu, A., Kim, D., Bissyand\u00e9, T.F.: TBar: revisiting template-based automated program repair. In: International Symposium on Software Testing and Analysis, ISSTA 2019 (2019). https:\/\/doi.org\/10.1145\/3293882.3330577","DOI":"10.1145\/3293882.3330577"},{"key":"1_CR41","unstructured":"Livshits, B.: SecuriBench Micro (2014). https:\/\/github.com\/too4words\/securibench-micro"},{"key":"1_CR42","doi-asserted-by":"publisher","unstructured":"Long, F., Rinard, M.C.: Automatic patch generation by learning correct code. In: Symposium on Principles of Programming Languages, POPL 2016 (2016). https:\/\/doi.org\/10.1145\/2837614.2837617","DOI":"10.1145\/2837614.2837617"},{"key":"1_CR43","doi-asserted-by":"publisher","unstructured":"Mechtaev, S., Yi, J., Roychoudhury, A.: DirectFix: looking for simple program repairs. In: International Conference on Software Engineering, ICSE 2015 (2015). https:\/\/doi.org\/10.1109\/ICSE.2015.63","DOI":"10.1109\/ICSE.2015.63"},{"key":"1_CR44","doi-asserted-by":"publisher","unstructured":"Mechtaev, S., Yi, J., Roychoudhury, A.: Angelix: scalable multiline program patch synthesis via symbolic analysis. In: International Conference on Software Engineering, ICSE 2016 (2016). https:\/\/doi.org\/10.1145\/2884781.2884807","DOI":"10.1145\/2884781.2884807"},{"key":"1_CR45","doi-asserted-by":"publisher","unstructured":"Ngo, M., Massacci, F., Milushev, D., Piessens, F.: Runtime enforcement of security policies on black box reactive programs. In: Symposium on Principles of Programming Languages, POPL 2015 (2015). https:\/\/doi.org\/10.1145\/2676726.2676978","DOI":"10.1145\/2676726.2676978"},{"key":"1_CR46","doi-asserted-by":"publisher","unstructured":"Nguyen, H.D.T., Qi, D., Roychoudhury, A., Chandra, S.: SemFix: program repair via semantic analysis. In: International Conference on Software Engineering, ICSE 2013 (2013). https:\/\/doi.org\/10.1109\/ICSE.2013.6606623","DOI":"10.1109\/ICSE.2013.6606623"},{"key":"1_CR47","doi-asserted-by":"publisher","DOI":"10.1145\/3408987","author":"N Polikarpova","year":"2020","unstructured":"Polikarpova, N., Stefan, D., Yang, J., Itzhaky, S., Hance, T., Solar-Lezama, A.: Liquid information flow control. Proc. ACM Program. Lang. (ICFP) (2020). https:\/\/doi.org\/10.1145\/3408987","journal-title":"Proc. ACM Program. Lang. (ICFP)"},{"key":"1_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/978-3-030-25543-5_5","volume-title":"Computer Aided Verification","author":"A Reynolds","year":"2019","unstructured":"Reynolds, A., Barbosa, H., N\u00f6tzli, A., Barrett, C., Tinelli, C.: cvc4sy: smart and fast term enumeration for syntax-guided synthesis. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 74\u201383. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_5"},{"key":"1_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-030-25540-4_9","volume-title":"Computer Aided Verification","author":"R Shemer","year":"2019","unstructured":"Shemer, R., Gurfinkel, A., Shoham, S., Vizel, Y.: Property directed self composition. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 161\u2013179. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_9"},{"key":"1_CR50","doi-asserted-by":"publisher","unstructured":"Smith, E.K., Barr, E.T., Goues, C.L., Brun, Y.: Is the cure worse than the disease? Overfitting in automated program repair. In: Joint Meeting on Foundations of Software Engineering, ESEC\/FSE 2015 (2015). https:\/\/doi.org\/10.1145\/2786805.2786825","DOI":"10.1145\/2786805.2786825"},{"key":"1_CR51","doi-asserted-by":"publisher","unstructured":"Tiraboschi, I., Rezk, T., Rival, X.: Sound symbolic execution via abstract interpretation and its application to security. In: International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2023 (2023). https:\/\/doi.org\/10.1007\/978-3-031-24950-1_13","DOI":"10.1007\/978-3-031-24950-1_13"},{"key":"1_CR52","doi-asserted-by":"publisher","unstructured":"Tsoupidi, R., Balliu, M., Baudry, B.: Vivienne: relational verification of cryptographic implementations in WebAssembly. In: Secure Development Conference, SecDev 2021 (2021). https:\/\/doi.org\/10.1109\/SECDEV51306.2021.00029","DOI":"10.1109\/SECDEV51306.2021.00029"},{"key":"1_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"742","DOI":"10.1007\/978-3-030-81685-8_35","volume-title":"Computer Aided Verification","author":"H Unno","year":"2021","unstructured":"Unno, H., Terauchi, T., Koskinen, E.: Constraint-based relational verification. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 742\u2013766. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_35"},{"key":"1_CR54","doi-asserted-by":"publisher","unstructured":"Wong, W.E., Gao, R., Li, Y., Abreu, R., Wotawa, F.: A survey on software fault localization. IEEE Trans. Softw. Eng. 42(8) (2016). https:\/\/doi.org\/10.1109\/TSE.2016.2521368","DOI":"10.1109\/TSE.2016.2521368"},{"key":"1_CR55","doi-asserted-by":"publisher","unstructured":"Xiong, Y., et al.: Precise condition synthesis for program repair. In: International Conference on Software Engineering, ICSE 2017 (2017). https:\/\/doi.org\/10.1109\/ICSE.2017.45","DOI":"10.1109\/ICSE.2017.45"},{"key":"1_CR56","doi-asserted-by":"publisher","unstructured":"Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: Computer Security Foundations Workshop, CSFW 2003 (2003). https:\/\/doi.org\/10.1109\/CSFW.2003.1212703","DOI":"10.1109\/CSFW.2003.1212703"},{"key":"1_CR57","doi-asserted-by":"publisher","unstructured":"Zhu, Q., et al.: A syntax-guided edit decoder for neural program repair. In: Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC\/FSE 2021 (2021). https:\/\/doi.org\/10.1145\/3468264.3468544","DOI":"10.1145\/3468264.3468544"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-65633-0_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:03:17Z","timestamp":1721890997000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65633-0_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656323","9783031656330"],"references-count":57,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65633-0_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"36","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}