{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:56:36Z","timestamp":1782867396978,"version":"3.54.5"},"publisher-location":"Cham","reference-count":17,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032227485","type":"print"},{"value":"9783032227492","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"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]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Modeling memory accurately is crucial for the verification of C\u00a0programs, but its inherent complexity limits scalability and efficiency. A memory model that abstracts unnecessary details while preserving essential information can significantly improve verification performance. In this work, we present a one-dimensional memory model that has recently been integrated into all software verifiers of the\n                    <jats:sc>Ultimate<\/jats:sc>\n                    tool family. Compared to our previous two-dimensional memory model, this abstraction trades some precision for improved efficiency. While it is not suitable for verifying memory safety properties, it enables more scalable reachability verification. An experimental evaluation on SV-COMP reachability benchmarks demonstrates that\n                    <jats:sc>Ultimate Automizer<\/jats:sc>\n                    solves up to 30.45\u00a0% more tasks when using the one-dimensional memory model.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-22749-2_37","type":"book-chapter","created":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T13:09:13Z","timestamp":1776258553000},"page":"589-594","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Ultimate Automizer with a One-Dimensional Memory Model"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-4794-958X","authenticated-orcid":false,"given":"Manuel","family":"Bentele","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-7716-3898","authenticated-orcid":false,"given":"Max","family":"Barth","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-9216-1801","authenticated-orcid":false,"given":"Marcel","family":"Ebbinghaus","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jan","family":"K\u00f6rner","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8947-5373","authenticated-orcid":false,"given":"Daniel","family":"Dietsch","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4252-3558","authenticated-orcid":false,"given":"Matthias","family":"Heizmann","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4885-0728","authenticated-orcid":false,"given":"Dominik","family":"Klumpp","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5656-306X","authenticated-orcid":false,"given":"Frank","family":"Sch\u00fcssele","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2540-9489","authenticated-orcid":false,"given":"Andreas","family":"Podelski","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,4,15]]},"reference":[{"key":"37_CR1","doi-asserted-by":"publisher","unstructured":"Barrett, C., et al.: CVC4. In: In: Gopalakrishnan, G., Qadeer, S. (eds) Computer Aided Verification. CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14","DOI":"10.1007\/978-3-642-22110-1_14"},{"issue":"1","key":"37_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10009-017-0469-y","volume":"21","author":"D Beyer","year":"2017","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Reliable benchmarking: requirements and solutions. STTT 21(1), 1\u201329 (2017). https:\/\/doi.org\/10.1007\/s10009-017-0469-y","journal-title":"STTT"},{"key":"37_CR3","doi-asserted-by":"publisher","unstructured":"Beyer, D., Strej\u010dek, J.: Improvements in software verification and witness validation: SV-COMP 2025. In: Gurfinkel, A., Heule, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2025. LNCS, pp. 151\u2013186. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-90660-2_9","DOI":"10.1007\/978-3-031-90660-2_9"},{"key":"37_CR4","doi-asserted-by":"crossref","unstructured":"Beyer, D., Strej\u010dek, J.: Evaluating software verifiers for C, Java, and SV-LIB (report on SV-COMP 2026). In: Proc. TACAS. Springer (2026)","DOI":"10.1007\/978-3-032-22749-2_23"},{"key":"37_CR5","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2013. LNCS, vol. 7795 pp. 93\u2013107. Springer, Heielberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"37_CR6","doi-asserted-by":"publisher","unstructured":"Dietsch, D., et al.: Ultimate Automizer SV-COMP\u00a02026 competition contribution (2025). https:\/\/doi.org\/10.5281\/zenodo.17735224","DOI":"10.5281\/zenodo.17735224"},{"key":"37_CR7","unstructured":"Fondazione Bruno Kessler, University of Trento: MathSAT\u00a05 website (2025). https:\/\/mathsat.fbk.eu. Retrieved 06 Dec 2025"},{"key":"37_CR8","doi-asserted-by":"publisher","unstructured":"Heizmann, M., Chen, Y.F., Dietsch, D., Greitschus, M., Hoenicke, J., Li, Y., Nutz, A., Musa, B., Schilling, C., Schindler, T., Podelski, A.: Ultimate Automizer and the search for perfect interpolants (competition contribution). In: Proc. TACAS. pp. 447\u2013451. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_30","DOI":"10.1007\/978-3-319-89963-3_30"},{"key":"37_CR9","doi-asserted-by":"publisher","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Proc. CAV. pp. 36\u201352. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_2","DOI":"10.1007\/978-3-642-39799-8_2"},{"key":"37_CR10","unstructured":"Microsoft Research: Z3 website (2025). https:\/\/www.microsoft.com\/en-us\/research\/project\/z3. Retrieved 06 Dec 2025"},{"key":"37_CR11","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Proc. TACAS. pp. 337\u2013340. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"37_CR12","doi-asserted-by":"publisher","unstructured":"Sch\u00fcssele, F., Bentele, M., Dietsch, D., Heizmann, M., Jiang, X., Klumpp, D., Podelski, A.: Ultimate Automizer and the abstraction of bitwise operations (competition contribution). In: Proc. TACAS. pp. 418\u2013423. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_31","DOI":"10.1007\/978-3-031-57256-2_31"},{"key":"37_CR13","unstructured":"Sinz, C., Falke, S., Merz, F.: A precise memory model for low-level bounded model checking. In: Proc. SSV. USENIX Association (2010). https:\/\/www.usenix.org\/conference\/ssv10\/precise-memory-model-low-level-bounded-model-checking"},{"key":"37_CR14","unstructured":"Stanford University, University of Iowa: CVC4 source code (2021). https:\/\/github.com\/CVC4\/CVC4-archived. Retrieved 06 Dec 2025"},{"key":"37_CR15","doi-asserted-by":"publisher","unstructured":"Trt\u00edk, M., Strej\u010dek, J.: Symbolic memory with pointers. In: Proc. ATVA. pp. 380\u2013395. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_27","DOI":"10.1007\/978-3-319-11936-6_27"},{"key":"37_CR16","unstructured":"University of Freiburg: Ultimate source code (2025). https:\/\/github.com\/ultimate-pa\/ultimate. Retrieved 06 Dec 2025"},{"key":"37_CR17","unstructured":"University of Freiburg: Ultimate website (2025). https:\/\/ultimate-pa.org. Retrieved 06 Dec 2025"}],"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-032-22749-2_37","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:21:58Z","timestamp":1782865318000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-22749-2_37"}},"subtitle":["(Competition Contribution)"],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032227485","9783032227492"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-22749-2_37","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"15 April 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"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":"Turin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 April 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/about\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}