{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T02:58:57Z","timestamp":1742957937086,"version":"3.40.3"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031198489"},{"type":"electronic","value":"9783031198496"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-19849-6_17","type":"book-chapter","created":{"date-parts":[[2022,10,19]],"date-time":"2022-10-19T15:03:32Z","timestamp":1666191812000},"page":"279-298","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Automated Repair of\u00a0Security Errors in\u00a0C Programs via\u00a0Statistical Model Checking: A Proof of\u00a0Concept"],"prefix":"10.1007","author":[{"given":"Khanh Huu The","family":"Dam","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fabien","family":"Duchene","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Given-Wilson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maxime","family":"Cordy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Axel","family":"Legay","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,10,17]]},"reference":[{"key":"17_CR1","unstructured":"GDB: The GNU Project Debugger. https:\/\/www.gnu.org\/software\/gdb\/. Accessed 14 Oct 2020"},{"key":"17_CR2","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-50086-3_1","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"D Basile","year":"2020","unstructured":"Basile, D., ter Beek, M.H., Legay, A.: Strategy synthesis for autonomous driving in a moving block railway system with Uppaal Stratego. In: Gotsman, A., Sokolova, A. (eds.) FORTE 2020. LNCS, vol. 12136, pp. 3\u201321. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-50086-3_1"},{"key":"17_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-642-40196-1_12","volume-title":"Quantitative Evaluation of Systems","author":"B Boyer","year":"2013","unstructured":"Boyer, B., Corre, K., Legay, A., Sedwards, S.: PLASMA-lab: a flexible, distributable statistical model checking library. In: Joshi, K., Siegle, M., Stoelinga, M., D\u2019Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 160\u2013164. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40196-1_12"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/978-3-030-84629-9_6","volume-title":"Model Checking Software","author":"A Chenoy","year":"2021","unstructured":"Chenoy, A., Duchene, F., Given-Wilson, T., Legay, A.: C-SMC: a hybrid statistical model checking and concrete runtime engine for analyzing C programs. In: Laarman, A., Sokolova, A. (eds.) SPIN 2021. LNCS, vol. 12864, pp. 101\u2013119. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-84629-9_6"},{"issue":"2","key":"17_CR6","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/s10703-009-0076-y","volume":"36","author":"EM Clarke","year":"2010","unstructured":"Clarke, E.M., Donz\u00e9, A., Legay, A.: On simulation-based probabilistic model checking of mixed-analog circuits. Formal Methods Syst. Des. 36(2), 97\u2013113 (2010)","journal-title":"Formal Methods Syst. Des."},{"key":"17_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-10575-8_1","volume-title":"Handbook of Model Checking","author":"EM Clarke","year":"2018","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H.: Introduction to model checking. In: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 1\u201326. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_1"},{"issue":"4","key":"17_CR8","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/s10009-014-0361-y","volume":"17","author":"A David","year":"2015","unstructured":"David, A., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B.: Uppaal SMC tutorial. Int. J. Softw. Tools Technol. Transf. 17(4), 397\u2013415 (2015)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"3","key":"17_CR9","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/s10009-014-0323-4","volume":"17","author":"A David","year":"2015","unstructured":"David, A., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B., Sedwards, S.: Statistical model checking for biological systems. Int. J. Softw. Tools Technol. Transf. 17(3), 351\u2013367 (2015)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: Sarkar, V., Hall, M.W. (eds.) Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, Chicago, IL, USA, 12\u201315 June 2005, pp. 213\u2013223. ACM (2005)","DOI":"10.1145\/1064978.1065036"},{"issue":"4","key":"17_CR11","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1109\/MS.2021.3072577","volume":"38","author":"CL Goues","year":"2021","unstructured":"Goues, C.L., Pradel, M., Roychoudhury, A., Chandra, S.: Automatic program repair. IEEE Softw. 38(4), 22\u201327 (2021)","journal-title":"IEEE Softw."},{"key":"17_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/978-3-642-40787-1_19","volume-title":"Runtime Verification","author":"K Havelund","year":"2013","unstructured":"Havelund, K.: A scala DSL for rete-based runtime verification. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 322\u2013327. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40787-1_19"},{"key":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-46002-0_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Havelund","year":"2002","unstructured":"Havelund, K., Ro\u015fu, G.: Synthesizing monitors for safety properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 342\u2013356. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-46002-0_24"},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-540-24622-0_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T H\u00e9rault","year":"2004","unstructured":"H\u00e9rault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 73\u201384. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24622-0_8"},{"key":"17_CR15","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/978-1-4612-0865-5_26","volume-title":"The Collected Works of Wassily Hoeffding","author":"W Hoeffding","year":"1994","unstructured":"Hoeffding, W.: Probability Inequalities for sums of Bounded Random Variables. In: Fisher, N.I., Sen, P.K. (eds.) The Collected Works of Wassily Hoeffding, pp. 409\u2013426. Springer, New York (1994). https:\/\/doi.org\/10.1007\/978-1-4612-0865-5_26"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/978-3-642-03845-7_15","volume-title":"Computational Methods in Systems Biology","author":"SK Jha","year":"2009","unstructured":"Jha, S.K., Clarke, E.M., Langmead, C.J., Legay, A., Platzer, A., Zuliani, P.: A Bayesian approach to model checking biological systems. In: Degano, P., Gorrieri, R. (eds.) CMSB 2009. LNCS, vol. 5688, pp. 218\u2013234. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03845-7_15"},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"Karakaya, K., Bodden, E.: Sootfx: a static code feature extraction tool for java and android. In: 21st IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2021, Luxembourg, 27\u201328 September 2021, pp. 181\u2013186. IEEE (2021)","DOI":"10.1109\/SCAM52516.2021.00030"},{"key":"17_CR18","doi-asserted-by":"crossref","unstructured":"Kulczynski, M., Legay, A., Nowotka, D., Poulsen, D.B.: Analysis of source code using UPPAAL. In: Proen\u00e7a, J., Paskevich, A. (eds.) Proceedings of the 6th Workshop on Formal Integrated Development Environment, F-IDE@NFM 2021, Held online, 24\u201325th May 2021. EPTCS, vol. 338, pp. 31\u201338 (2021)","DOI":"10.4204\/EPTCS.338.5"},{"key":"17_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-642-16612-9_11","volume-title":"Runtime Verification","author":"A Legay","year":"2010","unstructured":"Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 122\u2013135. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16612-9_11"},{"key":"17_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/978-3-319-91908-9_23","volume-title":"Computing and Software Science","author":"A Legay","year":"2019","unstructured":"Legay, A., Lukina, A., Traonouez, L.M., Yang, J., Smolka, S.A., Grosu, R.: Statistical model checking. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science. LNCS, vol. 10000, pp. 478\u2013504. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-319-91908-9_23"},{"key":"17_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-319-45994-3_2","volume-title":"Reachability Problems","author":"A Legay","year":"2016","unstructured":"Legay, A., Sedwards, S., Traonouez, L.-M.: Rare events for statistical model checking an overview. In: Larsen, K.G., Potapov, I., Srba, J. (eds.) RP 2016. LNCS, vol. 9899, pp. 23\u201335. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-45994-3_2"},{"key":"17_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-319-47166-2_6","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques","author":"A Legay","year":"2016","unstructured":"Legay, A., Sedwards, S., Traonouez, L.-M.: Plasma lab: a modular statistical model checking platform. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 77\u201393. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47166-2_6"},{"key":"17_CR23","doi-asserted-by":"crossref","unstructured":"Liu, K., Koyuncu, A., Bissyand\u00e9, T.F., Kim, D., Klein, J., Traon, Y.L.: You cannot fix what you cannot find! an investigation of fault localization bias in benchmarking automated program repair systems. In: 12th IEEE Conference on Software Testing, Validation and Verification, ICST 2019, Xi\u2019an, China, 22\u201327 April 2019, pp. 102\u2013113. IEEE (2019)","DOI":"10.1109\/ICST.2019.00020"},{"issue":"3","key":"17_CR24","doi-asserted-by":"publisher","first-page":"e1890","DOI":"10.1002\/smr.1890","volume":"30","author":"VC Ngo","year":"2018","unstructured":"Ngo, V.C., Legay, A.: Formal verification of probabilistic SystemC models with statistical model checking. J. Softw. Evol. Process. 30(3), e1890 (2018)","journal-title":"J. Softw. Evol. Process."},{"key":"17_CR25","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/BF02883985","volume":"10","author":"M Okamoto","year":"1959","unstructured":"Okamoto, M.: Some inequalities relating to the partial sum of binomial probabilities. Ann. Inst. Stat. Math. 10, 29\u201335 (1959)","journal-title":"Ann. Inst. Stat. Math."},{"issue":"2","key":"17_CR26","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/s11370-015-0169-y","volume":"8","author":"L Palopoli","year":"2015","unstructured":"Palopoli, L., et al.: Navigation assistance and guidance of older adults across complex public spaces: the DALi approach. Intell. Serv. Robot. 8(2), 77\u201392 (2015)","journal-title":"Intell. Serv. Robot."},{"key":"17_CR27","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), Providence, RI, USA, pp. 46\u201357. IEEE, September 1977","DOI":"10.1109\/SFCS.1977.32"},{"key":"17_CR28","series-title":"Adaptive Computation and Machine Learning","doi-asserted-by":"publisher","DOI":"10.1109\/TNN.1998.712192","volume-title":"Reinforcement Learning - An Introduction","author":"RS Sutton","year":"1998","unstructured":"Sutton, R.S., Barto, A.G.: Reinforcement Learning - An Introduction. Adaptive Computation and Machine Learning, MIT Press, Cambridge (1998)"},{"key":"17_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-642-30793-5_14","volume-title":"Formal Techniques for Distributed Systems","author":"S Tasharofi","year":"2012","unstructured":"Tasharofi, S., Karmani, R.K., Lauterburg, S., Legay, A., Marinov, D., Agha, G.: TransDPOR: a novel dynamic partial-order reduction technique for testing actor programs. In: Giese, H., Rosu, G. (eds.) FMOODS\/FORTE -2012. LNCS, vol. 7273, pp. 219\u2013234. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-30793-5_14"},{"key":"17_CR30","doi-asserted-by":"publisher","DOI":"10.1016\/j.cose.2021.102381","volume":"109","author":"MH ter Beek","year":"2021","unstructured":"ter Beek, M.H., Legay, A., Lluch-Lafuente, A., Vandin, A.: Quantitative security risk modeling and analysis with RisQFLan. Comput. Secur. 109, 102381 (2021)","journal-title":"Comput. Secur."},{"issue":"2","key":"17_CR31","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1214\/aoms\/1177731118","volume":"16","author":"A Wald","year":"1945","unstructured":"Wald, A.: Sequential tests of statistical hypotheses. Ann. Math. Stat. 16(2), 117\u2013186 (1945)","journal-title":"Ann. Math. Stat."},{"key":"17_CR32","doi-asserted-by":"crossref","unstructured":"Wen, W.: Software fault localization based on program slicing spectrum. In: Glinz, M., Murphy, G.C., Pezz\u00e8, M. (eds.) 34th International Conference on Software Engineering, ICSE 2012, 2\u20139 June 2012, Zurich, Switzerland, pp. 1511\u20131514. IEEE Computer Society (2012)","DOI":"10.1109\/ICSE.2012.6227049"},{"key":"17_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-45657-0_17","volume-title":"Computer Aided Verification","author":"HLS Younes","year":"2002","unstructured":"Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 223\u2013235. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_17"},{"key":"17_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/11513988_43","volume-title":"Computer Aided Verification","author":"HLS Younes","year":"2005","unstructured":"Younes, H.L.S.: Ymer: a statistical model checker. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 429\u2013433. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11513988_43"},{"issue":"2","key":"17_CR35","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/s10703-013-0195-3","volume":"43","author":"P Zuliani","year":"2013","unstructured":"Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to stateflow\/simulink verification. Formal Methods Syst. Des. 43(2), 338\u2013367 (2013)","journal-title":"Formal Methods Syst. Des."}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-19849-6_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,20]],"date-time":"2022-10-20T00:09:33Z","timestamp":1666224573000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-19849-6_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031198489","9783031198496"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-19849-6_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"17 October 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Leveraging Applications of Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rhodes","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 October 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 October 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.isola-conference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}