{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T02:22:13Z","timestamp":1769739733420,"version":"3.49.0"},"publisher-location":"Cham","reference-count":18,"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>\n            <jats:sc>Theta<\/jats:sc> is a model checking framework with a strong emphasis on effectively handling concurrency in software using abstraction refinement algorithms. In SV-COMP 2025, we complement our existing approach (abstraction-aware partial order reduction) for multi-threaded programs with a happens before propagator-based BMC check, expecting a significant increase in performance. We again utilize our portfolio with dynamic algorithm selection from last year, with improvements regarding solver choice and configuration ordering. In this paper, we detail our algorithmic improvements in <jats:sc>Theta<\/jats:sc> regarding the verification of concurrent software.<\/jats:p>","DOI":"10.1007\/978-3-031-90660-2_22","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T09:38:14Z","timestamp":1746005894000},"page":"260-265","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Theta: Various Approaches for Concurrent Program Verification (Competition Contribution)"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6260-5908","authenticated-orcid":false,"given":"Csan\u00e1d","family":"Telbisz","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6551-5860","authenticated-orcid":false,"given":"Levente","family":"Bajczi","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2912-028X","authenticated-orcid":false,"given":"D\u00e1niel","family":"Szekeres","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7617-3563","authenticated-orcid":false,"given":"Andr\u00e1s","family":"V\u00f6r\u00f6s","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"22_CR1","doi-asserted-by":"publisher","unstructured":"\u00c1d\u00e1m, Z., Bajczi, L., Dobos-Kov\u00e1cs, M., Hajdu, \u00c1., Moln\u00e1r, V.: Theta: portfolio of CEGAR-based analyses with dynamic algorithm selection (Competition Contribution). In: Fisman, D., Rosu, G. (eds.) TACAS 2022. Lecture Notes in Computer Science, vol. 13244, pp. 474\u2013478. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_34","DOI":"10.1007\/978-3-030-99527-0_34"},{"key":"22_CR2","doi-asserted-by":"publisher","unstructured":"Alglave, J., Kroening, D., Tautschnig, M.: Partial Orders for Efficient Bounded Model Checking of Concurrent Software. In: Sharygina, N., Veith, H. (eds.) CAV 2013. Lecture Notes in Computer Science, vol.\u00a08044, pp. 141\u2013157. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_9","DOI":"10.1007\/978-3-642-39799-8_9"},{"key":"22_CR3","doi-asserted-by":"publisher","unstructured":"Baier, D., Beyer, D., Friedberger, K.: Javasmt 3: Interacting with SMT solvers in java. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. Lecture Notes in Computer Science, vol. 12760, pp. 195\u2013208. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_9","DOI":"10.1007\/978-3-030-81688-9_9"},{"key":"22_CR4","doi-asserted-by":"publisher","unstructured":"Bajczi, L., Telbisz, C., Somorjai, M., \u00c1d\u00e1m, Z., Dobos-Kov\u00e1cs, M., Szekeres, D., Mondok, M., Moln\u00e1r, V.: Theta: Abstraction Based Techniques for Verifying Concurrency (Competition Contribution). In: TACAS 2024. Lecture Notes in Computer Science, vol. 14572, pp. 412\u2013417. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_30, https:\/\/doi.org\/10.1007\/978-3-031-57256-2_30","DOI":"10.1007\/978-3-031-57256-2_30"},{"key":"22_CR5","doi-asserted-by":"publisher","unstructured":"Bajczi, L., Telbisz, C., Somorjai, M., \u00c1d\u00e1m, Z., Dobos-Kov\u00e1cs, M., Szekeres, D., Moln\u00e1r, V.: Theta - SV-COMP\u201925 Verifier Archive (Nov 2024). https:\/\/doi.org\/10.5281\/zenodo.14194483","DOI":"10.5281\/zenodo.14194483"},{"key":"22_CR6","unstructured":"Bajczi, L., Telbisz, C., Szekeres, D., V\u00f6r\u00f6s, A.: On Stability in a Happens-Before Propagator for Concurrent Programs (Reproducibility Study). In: TACAS 2025. LNCS\u00a0, Springer (2025), https:\/\/ftsrg.mit.bme.hu\/paper-tacas25-ocfix\/paper.pdf"},{"key":"22_CR7","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et\u00a0al.: cvc5: A Versatile and Industrial-Strength SMT Solver. In: Fisman, D., Rosu, G. (eds.) TACAS 2022. pp. 415\u2013442. Springer International Publishing, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"22_CR8","unstructured":"Beyer, D., Strej\u010dek, J.: Improvements in software verification and witness validation: SV-COMP 2025. In: Proc. TACAS. LNCS, Springer (2025)"},{"key":"22_CR9","doi-asserted-by":"publisher","unstructured":"Bj\u00f8rner, N.S., Eisenhofer, C., Kov\u00e1cs, L.: Satisfiability Modulo Custom Theories in Z3. In: Dragoi, C., Emmi, M., Wang, J. (eds.) VMCAI 2023. Lecture Notes in Computer Science, vol. 13881, pp. 91\u2013105. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-24950-1_5","DOI":"10.1007\/978-3-031-24950-1_5"},{"key":"22_CR10","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B., Sebastiani, R.: The MathSAT5 SMT Solver. In: TACAS 2013, LNCS, vol.\u00a07795, pp. 93\u2013107. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"22_CR11","doi-asserted-by":"publisher","unstructured":"Hajdu, \u00c1., Micskei, Z.: Efficient Strategies for CEGAR-based Model Checking. Journal of Automated Reasoning 64(6), 1051\u20131091 (2020). https:\/\/doi.org\/10.1007\/s10817-019-09535-x","DOI":"10.1007\/s10817-019-09535-x"},{"key":"22_CR12","doi-asserted-by":"publisher","unstructured":"He, F., Sun, Z., Fan, H.: Deagle: An SMT-based Verifier for Multi-threaded Programs (Competition Contribution). In: Fisman, D., Rosu, G. (eds.) TACAS 2022. Lecture Notes in Computer Science, vol. 13244, pp. 424\u2013428. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_25","DOI":"10.1007\/978-3-030-99527-0_25"},{"key":"22_CR13","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver. In: TACAS 2008, LNCS, vol.\u00a04963, 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":"22_CR14","doi-asserted-by":"publisher","unstructured":"R\u00fcmmer, P.: A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic. LNCS, vol.\u00a05330, pp. 274\u2013289. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-89439-1_20","DOI":"10.1007\/978-3-540-89439-1_20"},{"key":"22_CR15","doi-asserted-by":"publisher","unstructured":"Sun, Z., Fan, H., He, F.: Consistency-preserving propagation for SMT solving of concurrent program verification. Proc. ACM Program. Lang. 6(OOPSLA2), 929\u2013956 (2022). https:\/\/doi.org\/10.1145\/3563321","DOI":"10.1145\/3563321"},{"key":"22_CR16","unstructured":"Telbisz, C.: Efficient automatic verification of concurrent programs. Master\u2019s thesis, Budapest University of Technology and Economics (2024), https:\/\/theta.mit.bme.hu\/publications\/telbiszcsMsc2024.pdf"},{"key":"22_CR17","doi-asserted-by":"publisher","unstructured":"T\u00f3th, T., Hajdu, \u00c1., V\u00f6r\u00f6s, A., Micskei, Z., Majzik, I.: Theta: a Framework for Abstraction Refinement-Based Model Checking. In: FMCAD 2017. pp. 176\u2013179 (2017). https:\/\/doi.org\/10.23919\/FMCAD.2017.8102257","DOI":"10.23919\/FMCAD.2017.8102257"},{"key":"22_CR18","doi-asserted-by":"publisher","unstructured":"Zennou, R., Atig, M.F., Biswas, R., Bouajjani, A., Enea, C., Erradi, M.: Boosting Sequential Consistency Checking Using Saturation. In: Hung, D.V., Sokolsky, O. (eds.) ATVA 2020. Lecture Notes in Computer Science, vol. 12302, pp. 360\u2013376. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_20","DOI":"10.1007\/978-3-030-59152-6_20"}],"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_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T09:38:17Z","timestamp":1746005897000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90660-2_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031906596","9783031906602"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90660-2_22","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":"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"}}]}}