https://m2.mtmt.hu/ hun 2026-06-24 17:21 JournalArticle 37085797 ADMIN_APPROVED true This research was partially funded by the EKOP-25-3 New National Excellence Program under project numbers EKÖP-25-3-BME-243, and EKÖP-25-3-BME-22, and the Doctoral Excellence Fellowship Programme under project numbers 400434/2023 and 400443/2023; funded by the NRDI Fund of Hungary. 0 false 2026-06-10T11:11:23.749+0000 2026-06-10T11:08:59.116+0000 2026-04-21T10:55:33.448+0000 true 10073063 Mondok Milán /api/author/10073063 Author Mondok Milán (informatika) true 2026-06-10T11:08:55.565+0000 2026-06-10T11:08:55.565+0000 2026-06-10T11:08:59.122+0000 true 10072271 Andódy Katalin /api/admin/10072271 Admin Andódy Katalin (BME admin4) true true false true 24 24 /api/publicationtype/24 PublicationType Folyóiratcikk 1 true 24 JournalArticle true 10000059 Article true 24 24 /api/publicationtype/24 PublicationType Folyóiratcikk 1 true 24 JournalArticle /api/subtype/10000059 Szakcikk SubType Szakcikk (Folyóiratcikk) 101 true 10000059 true 1 /api/category/1 Category Tudományos true 1 Mondok, Milán true true /api/journal/3029 REVIEWED LECTURE NOTES IN COMPUTER SCIENCE 0302-9743 1611-3349 true false 3029 false 3029 true 0302-9743 1611-3349 Journal FOREIGN 16506 510 515 Chapter 25 510, Chapter 25 6 2026 true 357881 /api/conference/357881 true 10843 true 10020 /api/country/10020 Country Olaszország true 16 /api/city/10843 City Turin, Olaszország true 1377641 Conference 32nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2026 2026-04-11 [Turin, Olaszország] true EmergenTheta is our sandbox for emerging analyses within the Theta framework. Previously established analyses have been migrated to Theta, and EmergenTheta focuses exclusively on novelties for both counterexample-guided abstraction refinement over control-flow automata and reachability analyses over symbolic transition systems. The 2026 submission presents a combined predicate–explicit abstraction domain, multithreaded symbolic transition system encodings, on-the-fly reachability and counterexample generation for generalized saturation, and an IC3 backend. This is the first year that we were able to submit EmergenTheta to all categories, representing a significant step in the evolution of Theta, and the competition results indicate the practical viability of the new techniques. © The Editor(s) (if applicable) and The Author(s), under exclusive license to Springer Nature Switzerland AG 2026. true true NATIONAL 2026 true true true true true false GOLD 2026-06-10 true https://doi.org/10.1007/978-3-032-22749-2_25 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 Q2 A false false false false 2026-06-09T11:08:17.974+0000 Mesterséges Intelligencia és Rendszertervezés T... (BME / VIK) 6 19 1 6 0 false Language 10002 /api/language/10002 Angol Angol English true 2 true PersonAuthorship 137360558 /api/authorship/137360558 Mondok, Milán ✉ [Mondok, Milán (informatika), szerző] Mesterséges Intelligencia és Rendszertervezés T... (BME / VIK) 1 0.167 true false true Author 10073063 /api/author/10073063 Mondok Milán (informatika) Mondok Milán true true Mondok Milán true false false AuthorshipType 1 /api/authorshiptype/1 Szerző 0 true 0 true false true PersonAuthorship 137360559 /api/authorship/137360559 Telbisz, Csanád [Telbisz, Csanád Ferenc (informatika), szerző] Mesterséges Intelligencia és Rendszertervezés T... (BME / VIK) 2 0.167 false false false Author 10094717 /api/author/10094717 Telbisz Csanád Ferenc (informatika) Telbisz Csanád Ferenc true true Telbisz Csanád true false false AuthorshipType 1 /api/authorshiptype/1 Szerző 0 true 0 true false true PersonAuthorship 137360560 /api/authorship/137360560 Bajczi, Levente [Bajczi, Levente (informatika), szerző] Mesterséges Intelligencia és Rendszertervezés T... (BME / VIK) 3 0.167 false false false Author 10073070 /api/author/10073070 Bajczi Levente (informatika) Bajczi Levente true true Bajczi Levente true false false AuthorshipType 1 /api/authorshiptype/1 Szerző 0 true 0 true false true PersonAuthorship 137360561 /api/authorship/137360561 Kovács, Dániel [Kovács, Dániel (Informatika), szerző] Mesterséges Intelligencia és Rendszertervezés T... (BME / VIK) 4 0.167 false false false Author 10105199 /api/author/10105199 Kovács Dániel (Informatika) Kovács Dániel true true Kovács Dániel true false false AuthorshipType 1 /api/authorshiptype/1 Szerző 0 true 0 true false true PersonAuthorship 137360562 /api/authorship/137360562 Dobos-Kovács, Mihály [Dobos-Kovács, Mihály (informatika), szerző] Mesterséges Intelligencia és Rendszertervezés T... (BME / VIK) 5 0.167 false false false Author 10073065 /api/author/10073065 Dobos-Kovács Mihály (informatika) Dobos-Kovács Mihály true true Dobos-Kovács Mihály true false false AuthorshipType 1 /api/authorshiptype/1 Szerző 0 true 0 true false true PersonAuthorship 137360563 /api/authorship/137360563 Molnár, Vince [Molnár, Vince (informatika), szerző] Mesterséges Intelligencia és Rendszertervezés T... (BME / VIK) 6 0.167 false true false Author 10049620 /api/author/10049620 Molnár Vince (informatika) Molnár Vince true 10049620 true Molnár Vince true false false AuthorshipType 1 /api/authorshiptype/1 Szerző 0 true 0 true false true PublicationIdentifier 31869902 /api/publicationidentifier/31869902 DOI: 10.1007/978-3-032-22749-2_25 PlainSource 6 /api/publicationsource/6 DOI PublicationSourceType 10001 /api/publicationsourcetype/10001 DOI true true true DOI DOI https://doi.org/@@@ true true 6 true GOLD true IDENTICAL 10.1007/978-3-032-22749-2_25 https://doi.org/10.1007/978-3-032-22749-2_25 false true PublicationIdentifier 32486091 /api/publicationidentifier/32486091 Scopus: 105039645560 PlainSource 3 /api/publicationsource/3 Scopus PublicationSourceType 10003 /api/publicationsourcetype/10003 Indexelő adatbázis false true true Scopus Scopus http://www.scopus.com/record/display.url?origin=inward&eid=2-s2.0-@@@ true true 3 true 105039645560 http://www.scopus.com/record/display.url?origin=inward&eid=2-s2.0-105039645560 false true PublicationIdentifier 31869903 /api/publicationidentifier/31869903 Egyéb URL: https://link.springer.com/10.1007/978-3-032-22749-2_25 PlainSource 40 /api/publicationsource/40 Egyéb URL PublicationSourceType 10006 /api/publicationsourcetype/10006 Link true true true Egyéb URL Other URL @@@ true true 40 true https://link.springer.com/10.1007/978-3-032-22749-2_25 https://link.springer.com/10.1007/978-3-032-22749-2_25 false true Classification 10047 /api/classification/10047 Szoftvermérnökség, operációs rendszerek, gépi nyelvek true true MtaRating 11435124 /api/mtarating/11435124 X. Földtudományok Osztálya:A LECTURE NOTES IN COMPUTER SCIENCE 0302-9743 1611-3349 RatingType 10031 /api/ratingtype/10031 X. Földtudományok Osztálya X. FTO Institute 70 /api/institute/70 X. Földtudományok Osztálya XFO 0 false false false X. Földtudományok Osztálya HAS Section of Earth Sciences (X.) true 70 true true true A true true SjrRating 11676862 /api/sjrrating/11676862 sjr:Q2 (2026) Scopus - Computer Science (miscellaneous) LECTURE NOTES IN COMPUTER SCIENCE 0302-9743 1611-3349 167 0.49 book series RatingType 10002 /api/ratingtype/10002 sjr sjr true true ClassificationExternal 1701 /api/classificationexternal/1701 Scopus - Computer Science (miscellaneous) true 1701 true Q2 FROM_LAST_YEAR true true Reference 74724454 /api/reference/74724454 1. Baier, D., Beyer, D., Friedberger, K.: JavaSMT 3: Interacting with SMT Solvers in Java. In: Silva, A., Leino, K.R.M. (eds.) Computer Aided Verification. Lecture Notes in Computer Science, vol. 12760, pp. 195–208. Springer International Publishing, Cham (2021). https://doi.org/10.1007/978-3-030-81688-9_9, DOI: 10.1007/978-3-030-81688-9_9 1 10.1007/978-3-030-81688-9_9 false true Reference 74724455 /api/reference/74724455 2. Bajczi, L., Ádám, Z., Molnár, V.: C for Yourself: Comparison of Front-End Techniques for Formal Verification. In: 10th FormaliSEICSE 2022. pp. 1–11. ACM (2022https://doi.org/10.1145/3524482.3527646, DOI: 10.1145/3524482.3527646 2 10.1145/3524482.3527646 false true Reference 74724456 /api/reference/74724456 3. Barbosa, H., Barrett, C., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., Nötzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: cvc5: A Versatile and Industrial-Strength SMT Solver. In: Fisman, D., Rosu, G. (eds.) TACAS 2022. pp. 415–442. 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 3 10.1007/978-3-030-99524-9_24 false true Reference 74724457 /api/reference/74724457 4. Beyer, D., Strec̨jek, J.: Evaluating software verifiers for C, Java, and SV-LIB (report on SV-COMP 2026). In: Proc. TACAS (2). LNCS 16506, Springer (2026) 4 false true Reference 74724458 /api/reference/74724458 5. Beyer, D., Jankola, M., Lingsch-Rosenfeld, M., Xia, T., Zheng, X.: A modular program-transformation framework for reducing specifications to reachability (2025), https://arxiv.org/abs/2501.16310, DOI: 10.1007/978-3-032-06847-7_1 5 10.1007/978-3-032-06847-7_1 false true Reference 74724459 /api/reference/74724459 6. Biere, A., Artho, C., Schuppan, V.: Liveness checking as safety checking. In: FMICS 2002, ICALP 2002 Satellite Workshop (2002).https://doi.org/10.1016/S1571-0661(04)80410-9, DOI: 10.1016/S1571-0661(04)80410-9 6 10.1016/S1571-0661(04)80410-9 false true Reference 74724460 /api/reference/74724460 7. Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking without BDDs. In: TACAS (1999https://doi.org/10.1007/3-540-49059-0_14, DOI: 10.1007/3-540-49059-0_14 7 10.1007/3-540-49059-0_14 false true Reference 74724461 /api/reference/74724461 8. Cimatti, A., Griggio, A., Schaafsma, B., Sebastiani, R.: The MathSAT5 SMT Solver. In: TACAS 2013, LNCS, vol. 7795, pp. 93–107. Springer (2013).https://doi.org/10.1007/978-3-642-36742-7_7, DOI: 10.1007/978-3-642-36742-7_7 8 10.1007/978-3-642-36742-7_7 false true Reference 74724462 /api/reference/74724462 9. Dobos-Kovács, M., Vörös, A.: Evaluation of SMT solvers in abstraction-based software model checking. In: Proceedings of the 11th Latin-American Symposium on Dependable Computing. p. 109–116. LADC ’22, Association for Computing Machinery, New York, NY, USA (2023).https://doi.org/10.1145/3569902.3570187, DOI: 10.1145/3569902.3570187 9 10.1145/3569902.3570187 false true Reference 74724463 /api/reference/74724463 10. Een, N., Mishchenko, A., Brayton, R.: Efficient implementation of property directed reachability. In: Proceedings of the International Conference on Formal Methods in Computer-Aided Design. p. 125–134. FMCAD ’11, FMCAD Inc, Austin, Texas (2011), https://dl.acm.org/doi/10.5555/2157654.2157675 10 false true Reference 74724464 /api/reference/74724464 11. Hajdu, Á., Micskei, Z.: Efficient Strategies for CEGAR-based Model Checking. J. Autom. Reason. 64(6), 1051–1091 (2020). https://doi.org/10.1007/s10817-019-09535-x, DOI: 10.1007/s10817-019-09535-x 11 10.1007/s10817-019-09535-x false true Reference 74724465 /api/reference/74724465 12. Molnár, V., Majzik, I.: Saturation Enhanced with Conditional Locality: Application to Petri Nets. In: Donatelli, S., Haar, S. (eds.) Application and Theory of Petri Nets and Concurrency, pp. 342–361. Springer International Publishing, Cham (2019), DOI: 10.1007/978-3-030-21571-2_19 12 10.1007/978-3-030-21571-2_19 false true Reference 74724466 /api/reference/74724466 13. Mondok, M.: Efficient formal verification of component-based engineering models. Master’s thesis, Budapest University of Technology and Economics (2022) 13 false true Reference 74724467 /api/reference/74724467 14. Mondok, M., Molnár, V.: Efficient Manipulation of Logical Formulas as Decision Diagrams. In: Renczes, B. (ed.) Proceedings of the 31st PhD Mini-Symposium. pp. 61–65. Budapest University of Technology and Economics, Department of Measurement and Information Systems (2024).https://doi.org/10.3311/MINISY2024-012, DOI: 10.3311/MINISY2024-012 14 10.3311/MINISY2024-012 false true Reference 74724468 /api/reference/74724468 15. Mondok, M., Vörös, A.: Abstraction-based model checking of linear temporal properties. In: Renczes, B. (ed.) Proceedings of the 27th PhD Mini-Symposium. pp. 29–32. Budapest University of Technology and Economics, Department of Measurement and Information Systems (2020) 15 false true Reference 74724469 /api/reference/74724469 16. de Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver. In: TACAS 2008, LNCS, vol. 4963, pp. 337–340. Springer (2008).https://doi.org/10.1007/978-3-540-78800-3_24, DOI: 10.1007/978-3-540-78800-3_24 16 10.1007/978-3-540-78800-3_24 false true Reference 74724470 /api/reference/74724470 17. Tonetta, S.: Abstract Model Checking without Computing the Abstraction. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009: Formal Methods, pp. 89–105. Springer, Berlin Heidelberg, Berlin, Heidelberg (2009), DOI: 10.1007/978-3-642-05089-3_7 17 10.1007/978-3-642-05089-3_7 false true Reference 74724471 /api/reference/74724471 18. Ádám, Z., Bajczi, L., Dobos-Kovács, M., Molnár, V., Mondok, M., Somorjai, M., Szekeres, D., Telbisz, C., Kovács, D., Rippl, B.R.: Emergentheta - verifier archive (2025). https://doi.org/10.5281/zenodo.17779912, DOI: 10.5281/zenodo.17779912 18 10.5281/zenodo.17779912 false true /api/publication/37085797 Mondok Milán et al. EmergenTheta: Experimental Analyses within the Theta Framework (Competition Contribution). (2026) LECTURE NOTES IN COMPUTER SCIENCE 0302-9743 1611-3349 16506 510-515<div class="JournalArticle Publication long-list"> <div class="authors"> <img title="Forrásközlemény" style="float: left" src="/frontend/resources/grid/publication-core-icon.png"> <div class="autype autype0"> <span class="author-name" mtid="10073063"><a href="/gui2/?type=authors&mode=browse&sel=10073063" target="_blank">Mondok Milán ✉ (<span class="authorship-author-name">Mondok Milán</span> <span class="authorAux-mtmt"> informatika</span>) </a> </span> <span class="author-affil"><span title="Budapesti Műszaki és Gazdaságtudományi Egyetem">BME</span>/<span title="Villamosmérnöki és Informatikai Kar">VIK</span>/Mesterséges Intelligencia és Rendszertervezés Tanszék</span> ;&nbsp;&nbsp;&nbsp; <span class="author-name" mtid="10094717"><a href="/gui2/?type=authors&mode=browse&sel=10094717" target="_blank">Telbisz Csanád (<span class="authorship-author-name">Telbisz Csanád Ferenc</span> <span class="authorAux-mtmt"> informatika</span>) </a> </span> <span class="author-affil"><span title="Budapesti Műszaki és Gazdaságtudományi Egyetem">BME</span>/<span title="Villamosmérnöki és Informatikai Kar">VIK</span>/Mesterséges Intelligencia és Rendszertervezés Tanszék</span> ;&nbsp;&nbsp;&nbsp; <span class="author-name" mtid="10073070"><a href="/gui2/?type=authors&mode=browse&sel=10073070" target="_blank">Bajczi Levente (<span class="authorship-author-name">Bajczi Levente</span> <span class="authorAux-mtmt"> informatika</span>) </a> </span> <span class="author-affil"><span title="Budapesti Műszaki és Gazdaságtudományi Egyetem">BME</span>/<span title="Villamosmérnöki és Informatikai Kar">VIK</span>/Mesterséges Intelligencia és Rendszertervezés Tanszék</span> ;&nbsp;&nbsp;&nbsp; <span class="author-name" mtid="10105199"><a href="/gui2/?type=authors&mode=browse&sel=10105199" target="_blank">Kovács Dániel (<span class="authorship-author-name">Kovács Dániel</span> <span class="authorAux-mtmt"> Informatika</span>) </a> </span> <span class="author-affil"><span title="Budapesti Műszaki és Gazdaságtudományi Egyetem">BME</span>/<span title="Villamosmérnöki és Informatikai Kar">VIK</span>/Mesterséges Intelligencia és Rendszertervezés Tanszék</span> ;&nbsp;&nbsp;&nbsp; <span class="author-name" mtid="10073065"><a href="/gui2/?type=authors&mode=browse&sel=10073065" target="_blank">Dobos-Kovács Mihály (<span class="authorship-author-name">Dobos-Kovács Mihály</span> <span class="authorAux-mtmt"> informatika</span>) </a> </span> <span class="author-affil"><span title="Budapesti Műszaki és Gazdaságtudományi Egyetem">BME</span>/<span title="Villamosmérnöki és Informatikai Kar">VIK</span>/Mesterséges Intelligencia és Rendszertervezés Tanszék</span> ;&nbsp;&nbsp;&nbsp; <span class="author-name" mtid="10049620"><a href="/gui2/?type=authors&mode=browse&sel=10049620" target="_blank">Molnár Vince (<span class="authorship-author-name">Molnár Vince</span> <span class="authorAux-mtmt"> informatika</span>) </a> </span> <span class="author-affil"><span title="Budapesti Műszaki és Gazdaságtudományi Egyetem">BME</span>/<span title="Villamosmérnöki és Informatikai Kar">VIK</span>/Mesterséges Intelligencia és Rendszertervezés Tanszék</span> </div> </div> <div class="title"><a href="/gui2/?mode=browse&params=publication;37085797" target="_blank">EmergenTheta: Experimental Analyses within the Theta Framework (Competition Contribution)</a></div> <div> <span class="journal-title">LECTURE NOTES IN COMPUTER SCIENCE</span> <span class="journal-issn">(<a target="_blank" href="https://portal.issn.org/resource/ISSN/0302-9743">0302-9743</a> <a target="_blank" href="https://portal.issn.org/resource/ISSN/1611-3349">1611-3349</a>)</span>: <span class="journal-volume">16506</span> <span class="page"> pp 510-515 Paper Chapter 25. </span> <span class="year">(2026)</span> <div class="conference"> 32nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2026. Konferencia helye, ideje: <span class="location">Turin, Olaszország <span class="conference-date">2026.04.11. - 2026.04.16.</span> </div> </div> <div class="pub-footer"> <span class="language" xmlns="http://www.w3.org/1999/html">Nyelv: Angol | </span> <span class="identifiers"> <span class="id identifier oa_GOLD" title=" Gold "> <a style="color:blue" title="10.1007/978-3-032-22749-2_25" target="_blank" href="https://doi.org/10.1007/978-3-032-22749-2_25"> DOI </a> </span> <span class="id identifier oa_none" title="none"> <a style="color:black" title="105039645560" target="_blank" href="http://www.scopus.com/record/display.url?origin=inward&eid=2-s2.0-105039645560"> Scopus </a> </span> <span class="id identifier oa_none" title="none"> <a style="color:black" title="https://link.springer.com/10.1007/978-3-032-22749-2_25" target="_blank" href="https://link.springer.com/10.1007/978-3-032-22749-2_25"> Egyéb URL </a> </span> </span> <OnlyViewableByAuthor><div class="ratings"> <div class="journal-subject">Folyóirat szakterülete: Scopus - Computer Science (miscellaneous)&nbsp;&nbsp;&nbsp;SJR indikátor:&nbsp;Q2</div> <div class="journal-subject">Folyóirat szakterülete: Scopus - Theoretical Computer Science&nbsp;&nbsp;&nbsp;SJR indikátor:&nbsp;Q3</div> <div class="journal-subject">X. Földtudományok Osztálya XFO&nbsp;&nbsp;&nbsp;A</div> </div></OnlyViewableByAuthor> <div class="mtid"><span class="long-pub-mtid">Közlemény: 37085797</span> | <span class="status-data status-ADMIN_APPROVED"> Admin láttamozott </span> Forrás | <span class="type-subtype">Folyóiratcikk ( Szakcikk ) </span> | <span class="pub-category">Tudományos</span> | <span class="publication-sourceOfData">DOI XML</span> </div> <div class="lastModified">Utolsó módosítás: 2026.06.10. 13:08 Andódy Katalin (BME admin4) </div> <pre class="comment" style="margin-top: 0; margin-bottom: 0;"><u>Megjegyzés</u>: This research was partially funded by the EKOP-25-3 New National Excellence Program under project numbers EKÖP-25-3-BME-243, and EKÖP-25-3-BME-22, and the Doctoral Excellence Fellowship Programme under project numbers 400434/2023 and 400443/2023; funded by the NRDI Fund of Hungary.</pre> </div></div>