{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:09:34Z","timestamp":1776305374264,"version":"3.50.1"},"publisher-location":"Cham","reference-count":13,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031906596","type":"print"},{"value":"9783031906602","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>The Static Value-Flow Analysis Framework (SVF) is a tool that enables interprocedural static value-flow analysis for LLVM-based languages by leveraging sparse and on-demand analysis. This work, SVF-SVC, presents an adaptation of SVF for its debut in SV-COMP 2025. We detail our development which uses SVF as a library to correctly parse SV-COMP program specifications and produce witnesses statements for C programs in the ReachSafety, MemSafety and SoftwareSystems categories. We evaluate SVF-SVC\u2019s performance in SV-COMP 2025 and pave the way for its participation in future editions.\n<\/jats:p>","DOI":"10.1007\/978-3-031-90660-2_21","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T09:38:07Z","timestamp":1746005887000},"page":"254-259","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["SVF-SVC: Software Verification Using SVF (Competition Contribution)"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-9983-9401","authenticated-orcid":false,"given":"Cameron","family":"McGowan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthew","family":"Richards","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9510-6574","authenticated-orcid":false,"given":"Yulei","family":"Sui","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"21_CR1","unstructured":"Andersen, L.O., Lee, P.: Program analysis and specialization for the c programming language (2005), https:\/\/api.semanticscholar.org\/CorpusID:20876553"},{"key":"21_CR2","unstructured":"Beyer, D., Strej\u010dek, J.: Improvements in software verification and witness validation: SV-COMP 2025. In: Proc. TACAS. LNCS, Springer (2025)"},{"key":"21_CR3","doi-asserted-by":"publisher","unstructured":"Cheng, X., Wang, J., Sui, Y.: Precise sparse abstract execution via cross-domain interaction. In: Proceedings of the IEEE\/ACM 46th International Conference on Software Engineering. ICSE \u201924, Association for Computing Machinery, New York, NY, USA (2024). https:\/\/doi.org\/10.1145\/3597503.3639220","DOI":"10.1145\/3597503.3639220"},{"key":"21_CR4","doi-asserted-by":"publisher","unstructured":"Chow, F., Chan, S., Liu, S.M., Lo, R., Streich, M.: Effective representation of aliases and indirect memory operations in ssa form (01 2000). https:\/\/doi.org\/10.1007\/3-540-61053-7_66","DOI":"10.1007\/3-540-61053-7_66"},{"key":"21_CR5","unstructured":"Lattner, C.: Llvm and clang: Next generation compiler technology. In: The BSD conference. vol.\u00a05, pp. 1\u201320 (2008)"},{"key":"21_CR6","doi-asserted-by":"crossref","unstructured":"Lattner, C., Adve, V.: Llvm: A compilation framework for lifelong program analysis & transformation. In: Proceedings of the International Symposium on Code Generation and Optimization: Feedback-Directed and Runtime Optimization. p.\u00a075. CGO \u201904, IEEE Computer Society, USA (2004)","DOI":"10.1109\/CGO.2004.1281665"},{"key":"21_CR7","unstructured":"Richards, M., McGowan, C.: Lasagnenator\/svf-svc-comp (2024), https:\/\/github.com\/Lasagnenator\/svf-svc-comp"},{"key":"21_CR8","doi-asserted-by":"publisher","unstructured":"Richards, M., McGowan, C.: svf-svc-comp: Release v1.4 (binaries) (Nov 2024). https:\/\/doi.org\/10.5281\/zenodo.14208597","DOI":"10.5281\/zenodo.14208597"},{"key":"21_CR9","doi-asserted-by":"publisher","unstructured":"Steffen, B., Knoop, J., R\u00fcthing, O.: The value flow graph: A program representation for optimal program transformations. vol.\u00a0432, pp. 389\u2013405 (01 2006). https:\/\/doi.org\/10.1007\/3-540-52592-0_76","DOI":"10.1007\/3-540-52592-0_76"},{"key":"21_CR10","doi-asserted-by":"publisher","unstructured":"Sui, Y., Xue, J.: Svf: interprocedural static value-flow analysis in llvm. In: Proceedings of the 25th International Conference on Compiler Construction. p. 265-266. CC \u201916, Association for Computing Machinery, New York, NY, USA (2016). https:\/\/doi.org\/10.1145\/2892208.2892235","DOI":"10.1145\/2892208.2892235"},{"key":"21_CR11","doi-asserted-by":"publisher","unstructured":"Sui, Y., Yan, H., Zheng, Z., Zhang, Y., Xue, J.: Parallel construction of interprocedural memory ssa form. Journal of Systems and Software 146, 186\u2013195 (2018). https:\/\/doi.org\/10.1016\/j.jss.2018.09.038","DOI":"10.1016\/j.jss.2018.09.038"},{"key":"21_CR12","doi-asserted-by":"publisher","unstructured":"Sui, Y., Ye, D., Xue, J.: Detecting memory leaks statically with full-sparse value-flow analysis. IEEE Transactions on Software Engineering 40(2), 107\u2013122 (2014). https:\/\/doi.org\/10.1109\/TSE.2014.2302311","DOI":"10.1109\/TSE.2014.2302311"},{"key":"21_CR13","doi-asserted-by":"publisher","unstructured":"Sui, Y., Ye, S., Xue, J., Yew, P.C.: Spas: scalable path-sensitive pointer analysis on full-sparse ssa. In: Proceedings of the 9th Asian Conference on Programming Languages and Systems. p. 155-171. APLAS\u201911, Springer-Verlag, Berlin, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-25318-8_14","DOI":"10.1007\/978-3-642-25318-8_14"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90660-2_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T09:38:16Z","timestamp":1746005896000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90660-2_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031906596","9783031906602"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90660-2_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","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":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}