{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T16:09:30Z","timestamp":1783008570294,"version":"3.54.5"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032071057","type":"print"},{"value":"9783032071064","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,10,6]],"date-time":"2025-10-06T00:00:00Z","timestamp":1759708800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,10,6]],"date-time":"2025-10-06T00:00:00Z","timestamp":1759708800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-07106-4_9","type":"book-chapter","created":{"date-parts":[[2025,10,7]],"date-time":"2025-10-07T14:38:12Z","timestamp":1759847892000},"page":"190-220","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Abstracting Concolic Execution for\u00a0Soft Contract Verification"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2924-3420","authenticated-orcid":false,"given":"Bram","family":"Vandenbogaerde","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9985-9808","authenticated-orcid":false,"given":"Quentin","family":"Sti\u00e9venart","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1710-1268","authenticated-orcid":false,"given":"Coen","family":"De Roover","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,10,6]]},"reference":[{"key":"9_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/11691617_10","volume-title":"Model Checking Software","author":"S Anand","year":"2006","unstructured":"Anand, S., P\u0103s\u0103reanu, C.S., Visser, W.: Symbolic execution with abstract subsumption checking. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 163\u2013181. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11691617_10"},{"key":"9_CR2","doi-asserted-by":"publisher","unstructured":"Anand, S., Pasareanu, C.S., Visser, W.: Symbolic execution with abstraction. Int. J. Softw. Tools Technol. Transf. 11(1), 53\u201367 (2009). https:\/\/doi.org\/10.1007\/S10009-008-0090-1","DOI":"10.1007\/S10009-008-0090-1"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 1\u20133 (2002)","DOI":"10.1145\/503272.503274"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Dimoulas, C., Findler, R.B., Flanagan, C., Felleisen, M.: Correct blame for contracts: no more scapegoating. In: Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on P rinciples of Programming Languages, POPL, 26\u201328 January 2011, pp. 215\u2013226. ACM (2011)","DOI":"10.1145\/1926385.1926410"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Dimoulas, C., Tobin-Hochstadt, S., Felleisen, M.: Complete monitors for behavioral contracts. In: Proceedings of the 21ste European Symposium on Programming Languages and Systems, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012. LNCS, vol. 7211, pp. 214\u2013233. Springer (2012)","DOI":"10.1007\/978-3-642-28869-2_11"},{"key":"9_CR7","doi-asserted-by":"publisher","unstructured":"Van Es, N., Sti\u00e9venart, Q., De Roover, C.: Garbage-free abstract interpretation through abstract reference counting. In: 33rd European Conference on Object-Oriented Programming, ECOOP. LIPIcs, 15\u201319 July 2019, vol. 134, pp. 10:1\u201310:33. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019). https:\/\/doi.org\/10.4230\/LIPICS.ECOOP.2019.10","DOI":"10.4230\/LIPICS.ECOOP.2019.10"},{"key":"9_CR8","doi-asserted-by":"publisher","unstructured":"Felleisen, M., Friedman, D.P.: A calculus for assignments in higher-order languages. In: Conference Record of the Fourteenth Annual ACM Symposium on Principles of Programming Languages, 21\u201323 January 1987, pp. 314\u2013325. ACM Press (1987). https:\/\/doi.org\/10.1145\/41625.41654","DOI":"10.1145\/41625.41654"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Findler, R.B., Felleisen, M.: Contracts for higher-order functions. In: Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming, pp. 48\u201359 (2002)","DOI":"10.1145\/581478.581484"},{"key":"9_CR10","doi-asserted-by":"publisher","unstructured":"Germane, K., McCarthy, J.: Newly-single and loving it: improving higher-order must-alias analysis with heap fragments. Proc. ACM Program. Lang. 5(ICFP), 1\u201328 (2021). https:\/\/doi.org\/10.1145\/3473601","DOI":"10.1145\/3473601"},{"key":"9_CR11","doi-asserted-by":"publisher","unstructured":"Glaze, D., Labich, N., Might, M., Van\u00a0Horn, D.: Optimizing abstract abstract machines. SIGPLAN Not. 48(9), 443\u2013454 (2013). https:\/\/doi.org\/10.1145\/2544174.2500604","DOI":"10.1145\/2544174.2500604"},{"key":"9_CR12","doi-asserted-by":"publisher","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: Proceedings of the 9th International Conference on Computer Aided Verification (CAV). LNCS, 22\u201325 June 1997, vol. 1254, pp. 72\u201383. Springer (1997). https:\/\/doi.org\/10.1007\/3-540-63166-6_10","DOI":"10.1007\/3-540-63166-6_10"},{"key":"9_CR13","doi-asserted-by":"publisher","unstructured":"Van Horn, D., Might, M.: Abstracting abstract machines. In: Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP 2010, 27\u201329 September 2010, pp. 51\u201362. ACM (2010). https:\/\/doi.org\/10.1145\/1863543.1863553","DOI":"10.1145\/1863543.1863553"},{"key":"9_CR14","unstructured":"Meyer, B.: Design by contract: the Eiffel method. In: 26th International Conference on Technology of Object-Oriented Languages and Systems (Tools), p. 446. IEEE Computer Society (1998)"},{"key":"9_CR15","doi-asserted-by":"publisher","unstructured":"Might, M., Shivers, O.: Improving flow analyses via GammaCFA: abstract garbage collection and counting. In: Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming, ICFP, 16\u201321 September 2006, pp. 13\u201325. ACM (2006). https:\/\/doi.org\/10.1145\/1159803.1159807","DOI":"10.1145\/1159803.1159807"},{"key":"9_CR16","doi-asserted-by":"publisher","unstructured":"Nguyen, P.C., Gilray, T., Tobin-Hochstadt, S., Van Horn, D.: Soft contract verification for higher-order stateful programs. Proc. ACM Program. Lang. 2(POPL), 51:1\u201351:30 (2018). https:\/\/doi.org\/10.1145\/3158139","DOI":"10.1145\/3158139"},{"key":"9_CR17","doi-asserted-by":"publisher","unstructured":"Nguyen, P.C., Tobin-Hochstadt, S., Van Horn, D.: Soft contract verification. In: Proceedings of the 19th ACM SIGPLAN International Conference on Functional programming, 1\u20133 September 2014, pp. 139\u2013152 (2014). https:\/\/doi.org\/10.1145\/2628136.2628156","DOI":"10.1145\/2628136.2628156"},{"key":"9_CR18","doi-asserted-by":"publisher","unstructured":"Nicolay, J., Sti\u00e9venart, Q., De Meuter, W., De Roover, C.: Effect-driven flow analysis. In: Proceedings of the 20th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI. LNCS, 13\u201315 January 2019, vol. 11388, pp. 247\u2013274. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-11245-5_12","DOI":"10.1007\/978-3-030-11245-5_12"},{"key":"9_CR19","doi-asserted-by":"publisher","unstructured":"Permenev, A., Dimitrov, D.K., Tsankov, P., Drachsler-Cohen, D., Vechev, M.T.: VerX: safety verification of smart contracts. In: 2020 IEEE Symposium on Security and Privacy, SP, 18\u201321 May 2020, pp. 1661\u20131677. IEEE (2020). https:\/\/doi.org\/10.1109\/SP40000.2020.00024","DOI":"10.1109\/SP40000.2020.00024"},{"key":"9_CR20","doi-asserted-by":"publisher","unstructured":"Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: Proceedings of the 10th European Software Engineering Conference held jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 5\u20139 September 2005, pp. 263\u2013272 (2005). https:\/\/doi.org\/10.1145\/1081706.1081750","DOI":"10.1145\/1081706.1081750"},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"Sen, K., Necula, G.C., Gong, L., Choi, W.: MultiSE: multi-path symbolic execution using value summaries. In: Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, ESEC\/FSE 2015, 30 August\u20134 September 2015, pp. 842\u2013853. ACM (2015)","DOI":"10.1145\/2786805.2786830"},{"key":"9_CR22","doi-asserted-by":"publisher","unstructured":"Sti\u00e9venart, Q., Van Es, N., Van der Plas, J., De Roover, C.: A parallel worklist algorithm and its exploration heuristics for static modular analyses. J. Syst. Softw. 181, 111042 (2021). https:\/\/doi.org\/10.1016\/J.JSS.2021.111042","DOI":"10.1016\/J.JSS.2021.111042"},{"key":"9_CR23","doi-asserted-by":"publisher","unstructured":"Tiraboschi, I., Rezk, T., Rival, X.: Sound symbolic execution via abstract interpretation and its application to security. In: Proceedings of the 24th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2023. LNCS, vol. 13881, pp. 267\u2013295. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-24950-1_13","DOI":"10.1007\/978-3-031-24950-1_13"},{"key":"9_CR24","doi-asserted-by":"publisher","unstructured":"Vandenbogaerde, B., Sti\u00e9venart, Q., De Roover, C.: Summary-based compositional analysis for soft contract verification. In: Proceedings of the 22nd IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2021, pp. 186\u2013196 (2021). https:\/\/doi.org\/10.1109\/SCAM55253.2022.00028","DOI":"10.1109\/SCAM55253.2022.00028"},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"Vandenbogaerde, B., Verbelen, S., Van Es, N., De Roover, C.: Monarch: a modular framework for abstract definitional interpreters in Haskell. In: Proceedings of the 32nd International Symposium on Static Analysis, SAS. LNCS, 12\u201318 October 2025. Springer (2025)","DOI":"10.1007\/978-3-032-07106-4_15"},{"key":"9_CR26","doi-asserted-by":"publisher","unstructured":"Vandercammen, M., De Roover, C.: State merging for concolic testing of event-driven applications. Sci. Comput. Program. 242, 103264 (2025). https:\/\/doi.org\/10.1016\/J.SCICO.2025.103264","DOI":"10.1016\/J.SCICO.2025.103264"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-07106-4_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T22:02:58Z","timestamp":1760047378000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-07106-4_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,6]]},"ISBN":["9783032071057","9783032071064"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-07106-4_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,6]]},"assertion":[{"value":"6 October 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Static Analysis Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Singapore","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Singapore","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 October 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 October 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sas2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/2025.splashcon.org\/home\/sas-2025","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}