https://m2.mtmt.hu/ eng 2026-07-28 10:00 JournalArticle 34768422 APPROVED true 0 false 2026-05-23T16:56:54.100+0000 2025-09-24T15:22:31.535+0000 2024-04-04T09:43:23.044+0000 true 10073063 Mondok Milán /api/author/10073063 Author Milán Mondok (informatika) true 2025-09-24T15:22:31.756+0000 2025-09-24T15:22:31.756+0000 true false true 24 24 /api/publicationtype/24 PublicationType Journal Article 1 true 24 JournalArticle true 10000059 Article true 24 24 /api/publicationtype/24 PublicationType Journal Article 1 true 24 JournalArticle /api/subtype/10000059 Szakcikk SubType Article (Journal Article) 101 true 10000059 true 1 /api/category/1 Category Scientific true 1 Bajczi, Levente 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 14572 371 375 Chapter 23 371, Chapter 23 5 2024 true 318724 /api/conference/318724 true 10913 true 10122 /api/country/10122 Country Luxembourg true 2151683 /api/city/10913 City Luxembourg, Luxembourg true 2015312 Conference 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2024, which was held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024 2024-04-06 [Luxembourg, Luxembourg] true Theta is a model checking framework conventionally based on abstraction refinement techniques. While abstraction is useful for a large number of verification problems, the over-reliance on the technique led to Theta being unable to meaningfully adapt. Identifying this problem in previous years of SV-COMP has led us to create EmergenTheta , a sandbox for the new approaches we want Theta to support. By differentiating between mature and emerging techniques, we can experiment more freely without hurting the reliability of the overall framework. In this paper we detail the development route to EmergenTheta , and its first debut on SV-COMP’24 in the ReachSafety category. true true 2024 true true true true true false GOLD 2026-05-23 true https://doi.org/10.1007/978-3-031-57256-2_23 1 1 1 1 0 1 1 1 1 1 1 1 1 1 0 0 1 1 1 1 0 2 2 Folyóiratcikk Journal Article 24 0 Könyvrészlet Chapter in Book 25 1 Könyv Book 23 0 Egyéb konferenciaközlemény Conference paper 31 0 Egyéb konferenciakötet Conference proceedings 32 0 Oltalmi formák Protection forms 26 0 Disszertáció Thesis 28 0 Egyéb Miscellaneous 29 0 Alkotás Achievement 22 0 Kutatási adat Research data 33 0 Folyóiratcikk Journal Article 24 0 0 0 Könyvrészlet Chapter in Book 25 0 0 0 Könyv Book 23 0 0 0 Egyéb konferenciaközlemény Conference paper 31 0 0 0 Egyéb konferenciakötet Conference proceedings 32 0 0 0 Oltalmi formák Protection forms 26 0 0 0 Disszertáció Thesis 28 0 0 0 Egyéb Miscellaneous 29 0 0 0 Alkotás Achievement 22 0 0 0 Kutatási adat Research data 33 0 0 0 2024 0 1 1 1 1 Q2 A false false false false 2024-07-03T09:43:24.055+0000 Kritikus Rendszerek Kutatócsoport (BME / VIK / MIT); Méréstechnika és Információs Rendszerek Tanszék (BME / VIK) 8 19 2 8 0 false Language 10002 /api/language/10002 English Angol English true 2 true PersonAuthorship 116011322 /api/authorship/116011322 Bajczi, Levente ✉ [Bajczi, Levente (informatika), author] Department of Measurement and Information Systems (BUTE / FEEI); Critical Systems Research Group (BUTE / FEEI / MIT) 1 0.125 true false true Author 10073070 /api/author/10073070 Levente Bajczi (informatika) Bajczi Levente true true Bajczi Levente true false false AuthorshipType 1 /api/authorshiptype/1 Author 0 true 0 true false true PersonAuthorship 116011323 /api/authorship/116011323 Szekeres, Dániel [Szekeres, Dániel (informatika), author] Department of Measurement and Information Systems (BUTE / FEEI); Critical Systems Research Group (BUTE / FEEI / MIT) 2 0.125 false false false Author 10078570 /api/author/10078570 Dániel Szekeres (informatika) Szekeres Dániel true true Szekeres Dániel true false false AuthorshipType 1 /api/authorshiptype/1 Author 0 true 0 true false true PersonAuthorship 116011324 /api/authorship/116011324 Mondok, Milán [Mondok, Milán (informatika), author] Department of Measurement and Information Systems (BUTE / FEEI); Critical Systems Research Group (BUTE / FEEI / MIT) 3 0.125 false false false Author 10073063 /api/author/10073063 Milán Mondok (informatika) Mondok Milán true true Mondok Milán true false false AuthorshipType 1 /api/authorshiptype/1 Author 0 true 0 true false true PersonAuthorship 116011325 /api/authorship/116011325 Ádám, Zsófia [Ádám, Zsófia (informatika), author] Department of Measurement and Information Systems (BUTE / FEEI); Critical Systems Research Group (BUTE / FEEI / MIT) 4 0.125 false false false Author 10077295 /api/author/10077295 Zsófia Ádám (informatika) Ádám Zsófia true true Ádám Zsófia true false false AuthorshipType 1 /api/authorshiptype/1 Author 0 true 0 true false true PersonAuthorship 116011326 /api/authorship/116011326 Somorjai, Márk [Somorjai, Márk (Informatika), author] Critical Systems Research Group (BUTE / FEEI / MIT) 5 0.125 false false false Author 10088738 /api/author/10088738 Márk Somorjai (Informatika) Somorjai Márk true true Somorjai Márk true false false AuthorshipType 1 /api/authorshiptype/1 Author 0 true 0 true false true PersonAuthorship 116011327 /api/authorship/116011327 Telbisz, Csanád [Telbisz, Csanád Ferenc (informatika), author] Department of Measurement and Information Systems (BUTE / FEEI); Critical Systems Research Group (BUTE / FEEI / MIT) 6 0.125 false false false Author 10094717 /api/author/10094717 Csanád Ferenc Telbisz (informatika) Telbisz Csanád Ferenc true true Telbisz Csanád true false false AuthorshipType 1 /api/authorshiptype/1 Author 0 true 0 true false true PersonAuthorship 116011328 /api/authorship/116011328 Dobos-Kovács, Mihály [Dobos-Kovács, Mihály (informatika), author] Department of Measurement and Information Systems (BUTE / FEEI); Critical Systems Research Group (BUTE / FEEI / MIT) 7 0.125 false false false Author 10073065 /api/author/10073065 Mihály Dobos-Kovács (informatika) Dobos-Kovács Mihály true true Dobos-Kovács Mihály true false false AuthorshipType 1 /api/authorshiptype/1 Author 0 true 0 true false true PersonAuthorship 116011329 /api/authorship/116011329 Molnár, Vince [Molnár, Vince (informatika), author] Department of Measurement and Information Systems (BUTE / FEEI); Critical Systems Research Group (BUTE / FEEI / MIT) 8 0.125 false true false Author 10049620 /api/author/10049620 Vince Molnár (informatika) Molnár Vince true 10049620 true Molnár Vince true false false AuthorshipType 1 /api/authorshiptype/1 Author 0 true 0 true false true PublicationIdentifier 25940149 /api/publicationidentifier/25940149 DOI: 10.1007/978-3-031-57256-2_23 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 10.1007/978-3-031-57256-2_23 https://doi.org/10.1007/978-3-031-57256-2_23 false true PublicationIdentifier 27376149 /api/publicationidentifier/27376149 WoS: 001284187100023 PlainSource 1 /api/publicationsource/1 WoS PublicationSourceType 10003 /api/publicationsourcetype/10003 Indexelő adatbázis false true true WoS WoS https://www.webofscience.com/wos/woscc/full-record/@@@ true true 1 true IDENTICAL 001284187100023 https://www.webofscience.com/wos/woscc/full-record/001284187100023 false true PublicationIdentifier 26198268 /api/publicationidentifier/26198268 Scopus: 85192239414 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 85192239414 http://www.scopus.com/record/display.url?origin=inward&eid=2-s2.0-85192239414 false true PublicationIdentifier 25940150 /api/publicationidentifier/25940150 Other URL: https://link.springer.com/10.1007/978-3-031-57256-2_23 PlainSource 40 /api/publicationsource/40 Other 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-031-57256-2_23 https://link.springer.com/10.1007/978-3-031-57256-2_23 false true MtaRating 11435124 /api/mtarating/11435124 X. Section of Earth Sciences:A LECTURE NOTES IN COMPUTER SCIENCE 0302-9743 1611-3349 RatingType 10031 /api/ratingtype/10031 X. Section of Earth Sciences X. FTO Institute 70 /api/institute/70 HAS Section of Earth Sciences (X.) HASSESX 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 11451949 /api/sjrrating/11451949 sjr:Q2 (2024) Scopus - Computer Science (miscellaneous) LECTURE NOTES IN COMPUTER SCIENCE 0302-9743 1611-3349 174 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 DIRECT true true Reference 51596190 /api/reference/51596190 1. Ádám, Z., Bajczi, L., Dobos-Kovács, M., Hajdu, Á., Molnár, V.: Theta: portfolio of CEGAR-based analyses with dynamic algorithm selection (Competition Contribution). In: Fisman, D., Rosu, G. (eds.) TACAS 2021. Lecture Notes in Computer Science, vol. 13244, pp. 474–478. Springer (2022). https://doi.org/10.1007/978-3-030-99527-0_34, DOI: 10.1007/978-3-030-99527-0_34 1 10.1007/978-3-030-99527-0_34 false true Reference 51596191 /api/reference/51596191 2. Bajczi, L., Szekeres, D., Mondok, M., Molnár, V.: EmergenTheta - SV-COMP’24 Verifier Archive (Nov 2023). https://doi.org/10.5281/zenodo.10198872, DOI: 10.5281/zenodo.10198872 2 10.5281/zenodo.10198872 false true Reference 51596192 /api/reference/51596192 3. Barrett, C., Tinelli, C.: Satisfiability Modulo Theories. https://doi.org/10.1007/978-3-319-10575-8_11, DOI: 10.1007/978-3-319-10575-8_11 3 10.1007/978-3-319-10575-8_11 false true Reference 51596193 /api/reference/51596193 4. Beyer, D.: State of the art in software verification and witness validation: SV-COMP 2024. In: Proc. TACAS. LNCS , Springer (2024) 4 false true Reference 51596194 /api/reference/51596194 5. Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking without BDDs. In: TACAS (1999). https://doi.org/10.1007/3-540-49059-0_14, DOI: 10.1007/3-540-49059-0_14 5 10.1007/3-540-49059-0_14 false true Reference 51596195 /api/reference/51596195 6. Hajdu, Á., Micskei, Z.: Efficient Strategies for CEGAR-based Model Checking. Journal of Automated Reasoning 64(6), 1051–1091 (2020). https://doi.org/10.1007/s10817-019-09535-x, DOI: 10.1007/s10817-019-09535-x 6 10.1007/s10817-019-09535-x false true Reference 51596196 /api/reference/51596196 7. McMillan, K.L.: Interpolation and SAT-Based Model Checking. In: Hunt, W.A., Somenzi, F. (eds.) Computer Aided Verification (2003). https://doi.org/10.1007/978-3-540-45069-6_1, DOI: 10.1007/978-3-540-45069-6_1 7 10.1007/978-3-540-45069-6_1 false true Reference 51596197 /api/reference/51596197 8. 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 8 10.1007/978-3-540-78800-3_24 false true Reference 51596198 /api/reference/51596198 9. Sheeran, M., Singh, S., Stålmarck, G.: Checking Safety Properties Using Induction and a SAT-Solver. In: Formal Methods in Computer-Aided Design (2000). https://doi.org/10.1007/3-540-40922-X_8, DOI: 10.1007/3-540-40922-X_8 9 10.1007/3-540-40922-X_8 false true Reference 51596199 /api/reference/51596199 10. Tóth’, T.: Abstraction Refinement-Based Verification of Timed Automata. Ph.D. thesis, Budapest University of Technology and Economics (2021) 10 false true /api/publication/34768422 Bajczi Levente et al. EmergenTheta: Verification Beyond Abstraction Refinement (Competition Contribution). (2024) LECTURE NOTES IN COMPUTER SCIENCE 0302-9743 1611-3349 14572 371-375<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"> <img title="Idézőközlemény" style="float: left" src="/frontend/resources/grid/publication-citation-icon.png"> <div class="autype autype0"> <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="Budapest University of Technology and Economics">BUTE</span>/<span title="Faculty of Electrical Engineering and Informatics">FEEI</span>/Department of Measurement and Information Systems; <span title="Budapest University of Technology and Economics">BUTE</span>/<span title="Faculty of Electrical Engineering and Informatics">FEEI</span>/<span title=" Department of Artificial Intelligence and Systems Engineering">MIT</span>/Critical Systems Research Group</span> ;&nbsp;&nbsp;&nbsp; <span class="author-name" mtid="10078570"><a href="/gui2/?type=authors&mode=browse&sel=10078570" target="_blank">Szekeres Dániel (<span class="authorship-author-name">Szekeres Dániel</span> <span class="authorAux-mtmt"> informatika</span>) </a> </span> <span class="author-affil"><span title="Budapest University of Technology and Economics">BUTE</span>/<span title="Faculty of Electrical Engineering and Informatics">FEEI</span>/Department of Measurement and Information Systems; <span title="Budapest University of Technology and Economics">BUTE</span>/<span title="Faculty of Electrical Engineering and Informatics">FEEI</span>/<span title=" Department of Artificial Intelligence and Systems Engineering">MIT</span>/Critical Systems Research Group</span> ;&nbsp;&nbsp;&nbsp; <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="Budapest University of Technology and Economics">BUTE</span>/<span title="Faculty of Electrical Engineering and Informatics">FEEI</span>/Department of Measurement and Information Systems; <span title="Budapest University of Technology and Economics">BUTE</span>/<span title="Faculty of Electrical Engineering and Informatics">FEEI</span>/<span title=" Department of Artificial Intelligence and Systems Engineering">MIT</span>/Critical Systems Research Group</span> ;&nbsp;&nbsp;&nbsp; <span class="author-name" mtid="10077295"><a href="/gui2/?type=authors&mode=browse&sel=10077295" target="_blank">Ádám Zsófia (<span class="authorship-author-name">Ádám Zsófia</span> <span class="authorAux-mtmt"> informatika</span>) </a> </span> <span class="author-affil"><span title="Budapest University of Technology and Economics">BUTE</span>/<span title="Faculty of Electrical Engineering and Informatics">FEEI</span>/Department of Measurement and Information Systems; <span title="Budapest University of Technology and Economics">BUTE</span>/<span title="Faculty of Electrical Engineering and Informatics">FEEI</span>/<span title=" Department of Artificial Intelligence and Systems Engineering">MIT</span>/Critical Systems Research Group</span> ;&nbsp;&nbsp;&nbsp; <span class="author-name" mtid="10088738"><a href="/gui2/?type=authors&mode=browse&sel=10088738" target="_blank">Somorjai Márk (<span class="authorship-author-name">Somorjai Márk</span> <span class="authorAux-mtmt"> Informatika</span>) </a> </span> <span class="author-affil"><span title="Budapest University of Technology and Economics">BUTE</span>/<span title="Faculty of Electrical Engineering and Informatics">FEEI</span>/<span title=" Department of Artificial Intelligence and Systems Engineering">MIT</span>/Critical Systems Research Group</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="Budapest University of Technology and Economics">BUTE</span>/<span title="Faculty of Electrical Engineering and Informatics">FEEI</span>/Department of Measurement and Information Systems; <span title="Budapest University of Technology and Economics">BUTE</span>/<span title="Faculty of Electrical Engineering and Informatics">FEEI</span>/<span title=" Department of Artificial Intelligence and Systems Engineering">MIT</span>/Critical Systems Research Group</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="Budapest University of Technology and Economics">BUTE</span>/<span title="Faculty of Electrical Engineering and Informatics">FEEI</span>/Department of Measurement and Information Systems; <span title="Budapest University of Technology and Economics">BUTE</span>/<span title="Faculty of Electrical Engineering and Informatics">FEEI</span>/<span title=" Department of Artificial Intelligence and Systems Engineering">MIT</span>/Critical Systems Research Group</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="Budapest University of Technology and Economics">BUTE</span>/<span title="Faculty of Electrical Engineering and Informatics">FEEI</span>/Department of Measurement and Information Systems; <span title="Budapest University of Technology and Economics">BUTE</span>/<span title="Faculty of Electrical Engineering and Informatics">FEEI</span>/<span title=" Department of Artificial Intelligence and Systems Engineering">MIT</span>/Critical Systems Research Group</span> </div> </div> <div class="title"><a href="/gui2/?mode=browse&params=publication;34768422" target="_blank">EmergenTheta: Verification Beyond Abstraction Refinement (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">14572</span> <span class="page"> pp 371-375 Paper Chapter 23. </span> <span class="year">(2024)</span> <div class="conference"> 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2024, which was held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024. Conference: <span class="location">Luxembourg, Luxembourg <span class="conference-date">2024.04.06. - 2024.04.11.</span> </div> </div> <div class="pub-footer"> <span class="language" xmlns="http://www.w3.org/1999/html">Language: English | </span> <span class="identifiers"> <span class="id identifier oa_GOLD" title=" Gold "> <a style="color:black" title="10.1007/978-3-031-57256-2_23" target="_blank" href="https://doi.org/10.1007/978-3-031-57256-2_23"> DOI </a> </span> <span class="id identifier oa_none" title="none"> <a style="color:blue" title="001284187100023" target="_blank" href="https://www.webofscience.com/wos/woscc/full-record/001284187100023"> WoS </a> </span> <span class="id identifier oa_none" title="none"> <a style="color:black" title="85192239414" target="_blank" href="http://www.scopus.com/record/display.url?origin=inward&eid=2-s2.0-85192239414"> Scopus </a> </span> <span class="id identifier oa_none" title="none"> <a style="color:black" title="https://link.springer.com/10.1007/978-3-031-57256-2_23" target="_blank" href="https://link.springer.com/10.1007/978-3-031-57256-2_23"> Other URL </a> </span> </span> <OnlyViewableByAuthor><div class="ratings"> <div class="journal-subject">Journal subject: Scopus - Computer Science (miscellaneous)&nbsp;&nbsp;&nbsp;Rank:&nbsp;Q2</div> <div class="journal-subject">Journal subject: Scopus - Theoretical Computer Science&nbsp;&nbsp;&nbsp;Rank:&nbsp;Q3</div> <div class="journal-subject">HAS Section of Earth Sciences (X.) HASSESX&nbsp;&nbsp;&nbsp;A</div> </div></OnlyViewableByAuthor> <div class="publication-citation" style="margin-left: 0.5cm;"> <span title="" class="citingPub-count">Citing papers: 1</span> | Independent citation: 1 | Self citation: 0 | Unknown citation: 0 | Number of citations in WoS: 1 | Number of citations in Scopus:&nbsp;1 | WoS/Scopus assigned:&nbsp;1 | Number of citations with DOI:&nbsp;1 (Not published:&nbsp;1) </div> <div class="publication-citation"> <a target="_blank" href="/api/publication?cond=citations.related;eq;34768422&sort=publishedYear,desc&sort=title"> Number of cited publications: 2 </a> </div> <div class="mtid"><span class="long-pub-mtid">Publication: 34768422</span> | <span class="status-data status-APPROVED"> Published </span> Core Citing | <span class="type-subtype">Journal Article ( Article ) </span> | <span class="pub-category">Scientific</span> | <span class="publication-sourceOfData">kézi felvitel</span> </div> <div class="lastModified">Last Modified: 2025.09.24. 17:22 Erika Szatmári (BME admin4) </div> </div></div>