var bibbase_data = {"data":"<img src=\"//bibbase.org/img/ajax-loader.gif\" id=\"spinner\"\n  style=\"display: none;\" alt=\"Loading..\" />\n\n<div id=\"bibbase\">\n\n  <script type=\"text/javascript\">\n    var bibbase = {\n      params: {\"bib\":\"https://leventebajczi.github.io/publications.bib\",\"jsonp\":\"1\",\"theme\":\"side\",\"host\":\"bibbase.org\"},\n      data: [{\"bibtype\":\"inproceedings\",\"type\":\"inproceedings\",\"title\":\"C for Yourself: Comparison of Front-End Techniques for Formal Verification\",\"author\":[{\"propositions\":[],\"lastnames\":[\"Bajczi\"],\"firstnames\":[\"Levente\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Ádám\"],\"firstnames\":[\"Zsófia\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Molnár\"],\"firstnames\":[\"Vince\"],\"suffixes\":[]}],\"booktitle\":\"2022 IEEE/ACM 10th International Conference on Formal Methods in Software Engineering (FormaliSE)\",\"doi\":\"10.1145/3524482.3527646\",\"unique-id\":\"32836583\",\"year\":\"2022\",\"orcid-numbers\":\"Bajczi, Levente/0000-0002-6551-5860; Ádám, Zsófia/0000-0003-2354-1750; Molnár, Vince/0000-0002-8204-7595\",\"abstract\":\"With the improvement of hardware and algorithms, the main challenge of software model checking has shifted from pure algorithmic performance toward supporting a wider set of input programs. Successful toolchains tackle the problem of parsing a wide range of inputs in an efficient way by reusing solutions from existing compiler technologies such as Eclipse CDT or LLVM. Our experience suggests that well-established techniques in compiler technology are not necessarily beneficial to model checkers and sometimes can even hurt their performance. In this paper, we review the tools mature enough to participate in the Software Verification Competition in terms of the employed analysis and frontend techniques. We find that successful tools do exhibit a bias toward certain combinations. We explore the theoretical reasons and suggest an adaptable approach for model checking frameworks. We validate our recommendations by implementing a new frontend for a model checking framework and show that it indeed benefits some of the algorithms.\",\"url_pdf\":\"https://leventebajczi.github.io/publications/formalise22.pdf\",\"url_slides\":\"https://leventebajczi.github.io/publications/slides/formalise22.pdf\",\"url_mtmt\":\"https://m2.mtmt.hu/api/publication/32836583\",\"bibtex\":\"@inproceedings{MTMT:32836583,\\n\\ttitle = {C for Yourself: Comparison of Front-End Techniques for Formal Verification},\\n\\tauthor = {Bajczi, Levente and Ádám, Zsófia and Molnár, Vince},\\n\\tbooktitle = {2022 IEEE/ACM 10th International Conference on Formal Methods in Software Engineering (FormaliSE)},\\n\\tdoi = {10.1145/3524482.3527646},\\n\\tunique-id = {32836583},\\n\\tyear = {2022},\\n\\torcid-numbers = {Bajczi, Levente/0000-0002-6551-5860; Ádám, Zsófia/0000-0003-2354-1750; Molnár, Vince/0000-0002-8204-7595},\\n\\tabstract = {With the improvement of hardware and algorithms, the main challenge of software model checking has shifted from pure algorithmic performance toward supporting a wider set of input programs. Successful toolchains tackle the problem of parsing a wide range of inputs in an efficient way by reusing solutions from existing compiler technologies such as Eclipse CDT or LLVM. Our experience suggests that well-established techniques in compiler technology are not necessarily beneficial to model checkers and sometimes can even hurt their performance. In this paper, we review the tools mature enough to participate in the Software Verification Competition in terms of the employed analysis and frontend techniques. We find that successful tools do exhibit a bias toward certain combinations. We explore the theoretical reasons and suggest an adaptable approach for model checking frameworks. We validate our recommendations by implementing a new frontend for a model checking framework and show that it indeed benefits some of the algorithms.},\\n\\n    url_pdf    = {https://leventebajczi.github.io/publications/formalise22.pdf},\\n    url_slides = {https://leventebajczi.github.io/publications/slides/formalise22.pdf},\\n\\turl_mtmt = {https://m2.mtmt.hu/api/publication/32836583},\\n}\\n\\n\",\"author_short\":[\"Bajczi, L.\",\"Ádám, Z.\",\"Molnár, V.\"],\"key\":\"MTMT:32836583\",\"id\":\"MTMT:32836583\",\"bibbaseid\":\"bajczi-dm-molnr-cforyourselfcomparisonoffrontendtechniquesforformalverification-2022\",\"role\":\"author\",\"urls\":{\" pdf\":\"https://leventebajczi.github.io/publications/formalise22.pdf\",\" slides\":\"https://leventebajczi.github.io/publications/slides/formalise22.pdf\",\" mtmt\":\"https://m2.mtmt.hu/api/publication/32836583\"},\"metadata\":{\"authorlinks\":{\"bajczi, l\":\"https://leventebajczi.com/publications.html\"}},\"downloads\":5,\"html\":\"\"},{\"bibtype\":\"article\",\"type\":\"article\",\"title\":\"Will My Program Break on This Faulty Processor?. Formal Analysis of Hardware Fault Activations in Concurrent Embedded Software\",\"author\":[{\"propositions\":[],\"lastnames\":[\"Bajczi\"],\"firstnames\":[\"Levente\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Vörös\"],\"firstnames\":[\"András\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Molnár\"],\"firstnames\":[\"Vince\"],\"suffixes\":[]}],\"doi\":\"10.1145/3358238\",\"journal-iso\":\"ACM T EMBED COMPUT S\",\"journal\":\"ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS\",\"volume\":\"18\",\"unique-id\":\"30865515\",\"issn\":\"1539-9087\",\"abstract\":\"Formal verification is approaching a point where it will be reliably applicable to embedded software. Even though formal verification can efficiently analyze multi-threaded applications, multi-core processors are often considered too dangerous to use in critical systems, despite the many benefits they can offer. One reason is the advanced memory consistency model of such CPUs. Nowadays, most software verifiers assume strict sequential consistency, which is also the naïve view of programmers. Modern multi-core processors, however, rarely guarantee this assumption by default. In addition, complex processor architectures may easily contain design faults. Thanks to the recent advances in hardware verification, these faults are increasingly visible and can be detected even in existing processors, giving an opportunity to compensate for the problem in software. In this paper, we propose a generic approach to consider inconsistent behavior of the hardware in the analysis of software. Our approach is based on formal methods and can be used to detect the activation of existing hardware faults on the application level and facilitate their mitigation in software. The approach relies heavily on recent results of model checking and hardware verification and offers new, integrative research directions. We propose a partial solution based on existing model checking tools to demonstrate feasibility and evaluate their performance in this context.\",\"year\":\"2019\",\"eissn\":\"1558-3465\",\"orcid-numbers\":\"Bajczi, Levente/0000-0002-6551-5860; Molnár, Vince/0000-0002-8204-7595\",\"url_pdf\":\"https://leventebajczi.github.io/publications/emsoft19.pdf\",\"url_slides\":\"https://leventebajczi.github.io/publications/slides/emsoft19.pdf\",\"url_mtmt\":\"https://m2.mtmt.hu/api/publication/30865515\",\"bibtex\":\"@article{MTMT:30865515,\\n\\ttitle = {Will My Program Break on This Faulty Processor?. Formal Analysis of Hardware Fault Activations in Concurrent Embedded Software},\\n\\tauthor = {Bajczi, Levente and Vörös, András and Molnár, Vince},\\n\\tdoi = {10.1145/3358238},\\n\\tjournal-iso = {ACM T EMBED COMPUT S},\\n\\tjournal = {ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS},\\n\\tvolume = {18},\\n\\tunique-id = {30865515},\\n\\tissn = {1539-9087},\\n\\tabstract = {Formal verification is approaching a point where it will be reliably applicable to embedded software. Even though formal verification can efficiently analyze multi-threaded applications, multi-core processors are often considered too dangerous to use in critical systems, despite the many benefits they can offer. One reason is the advanced memory consistency model of such CPUs. Nowadays, most software verifiers assume strict sequential consistency, which is also the naïve view of programmers. Modern multi-core processors, however, rarely guarantee this assumption by default. In addition, complex processor architectures may easily contain design faults. Thanks to the recent advances in hardware verification, these faults are increasingly visible and can be detected even in existing processors, giving an opportunity to compensate for the problem in software. In this paper, we propose a generic approach to consider inconsistent behavior of the hardware in the analysis of software. Our approach is based on formal methods and can be used to detect the activation of existing hardware faults on the application level and facilitate their mitigation in software. The approach relies heavily on recent results of model checking and hardware verification and offers new, integrative research directions. We propose a partial solution based on existing model checking tools to demonstrate feasibility and evaluate their performance in this context.},\\n\\tyear = {2019},\\n\\teissn = {1558-3465},\\n\\torcid-numbers = {Bajczi, Levente/0000-0002-6551-5860; Molnár, Vince/0000-0002-8204-7595},\\n\\n    url_pdf    = {https://leventebajczi.github.io/publications/emsoft19.pdf},\\n    url_slides = {https://leventebajczi.github.io/publications/slides/emsoft19.pdf},\\n\\turl_mtmt = {https://m2.mtmt.hu/api/publication/30865515},\\t\\n}\\n\\n\",\"author_short\":[\"Bajczi, L.\",\"Vörös, A.\",\"Molnár, V.\"],\"key\":\"MTMT:30865515\",\"id\":\"MTMT:30865515\",\"bibbaseid\":\"bajczi-vrs-molnr-willmyprogrambreakonthisfaultyprocessorformalanalysisofhardwarefaultactivationsinconcurrentembeddedsoftware-2019\",\"role\":\"author\",\"urls\":{\" pdf\":\"https://leventebajczi.github.io/publications/emsoft19.pdf\",\" slides\":\"https://leventebajczi.github.io/publications/slides/emsoft19.pdf\",\" mtmt\":\"https://m2.mtmt.hu/api/publication/30865515\"},\"metadata\":{\"authorlinks\":{\"bajczi, l\":\"https://leventebajczi.com/publications.html\"}},\"html\":\"\"},{\"bibtype\":\"article\",\"type\":\"article\",\"title\":\"Theta: portfolio of CEGAR-based analyses with dynamic algorithm selection (Competition Contribution)\",\"author\":[{\"propositions\":[],\"lastnames\":[\"Ádám\"],\"firstnames\":[\"Zsófia\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Bajczi\"],\"firstnames\":[\"Levente\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Dobos-Kovács\"],\"firstnames\":[\"Mihály\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Hajdu\"],\"firstnames\":[\"Ákos\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Molnár\"],\"firstnames\":[\"Vince\"],\"suffixes\":[]}],\"doi\":\"10.1007/978-3-030-99527-0_34\",\"journal-iso\":\"LECT NOTES COMPUT SC\",\"journal\":\"LECTURE NOTES IN COMPUTER SCIENCE\",\"volume\":\"13244\",\"unique-id\":\"32801008\",\"issn\":\"0302-9743\",\"keywords\":\"Computer Science, Software Engineering\",\"year\":\"2022\",\"eissn\":\"1611-3349\",\"pages\":\"474-478\",\"orcid-numbers\":\"Ádám, Zsófia/0000-0003-2354-1750; Bajczi, Levente/0000-0002-6551-5860; Dobos-Kovács, Mihály/0000-0002-0064-2965; Hajdu, Ákos/0000-0001-8001-8865; Molnár, Vince/0000-0002-8204-7595\",\"abstract\":\"THETA is a model checking framework based on abstraction refinement algorithms. In SV-COMP 2022, we introduce: 1) reasoning at the source-level via a direct translation from C programs; 2) support for concurrent programs with interleaving semantics; 3) mitigation for non-progressing refinement loops; 4) support for SMT-LIB-compliant solvers. We combine all of the aforementioned techniques into a portfolio with dynamic algorithm selection.\",\"url_pdf\":\"https://leventebajczi.github.io/publications/tacas22.pdf\",\"url_slides\":\"https://leventebajczi.github.io/publications/slides/tacas22.pdf\",\"url_poster\":\"https://leventebajczi.github.io/publications/posters/tacas22.pdf\",\"url_mtmt\":\"https://m2.mtmt.hu/api/publication/32801008\",\"bibtex\":\"@article{MTMT:32801008,\\n\\ttitle = {Theta: portfolio of CEGAR-based analyses with dynamic algorithm selection (Competition Contribution)},\\n\\tauthor = {Ádám, Zsófia and Bajczi, Levente and Dobos-Kovács, Mihály and Hajdu, Ákos and Molnár, Vince},\\n\\tdoi = {10.1007/978-3-030-99527-0_34},\\n\\tjournal-iso = {LECT NOTES COMPUT SC},\\n\\tjournal = {LECTURE NOTES IN COMPUTER SCIENCE},\\n\\tvolume = {13244},\\n\\tunique-id = {32801008},\\n\\tissn = {0302-9743},\\n\\tkeywords = {Computer Science, Software Engineering},\\n\\tyear = {2022},\\n\\teissn = {1611-3349},\\n\\tpages = {474-478},\\n\\torcid-numbers = {Ádám, Zsófia/0000-0003-2354-1750; Bajczi, Levente/0000-0002-6551-5860; Dobos-Kovács, Mihály/0000-0002-0064-2965; Hajdu, Ákos/0000-0001-8001-8865; Molnár, Vince/0000-0002-8204-7595},\\n\\tabstract = {THETA is a model checking framework based on abstraction refinement algorithms. In SV-COMP 2022, we introduce: 1) reasoning at the source-level via a direct translation from C programs; 2) support for concurrent programs with interleaving semantics; 3) mitigation for non-progressing refinement loops; 4) support for SMT-LIB-compliant solvers. We combine all of the aforementioned techniques into a portfolio with dynamic algorithm selection.},\\n\\n    url_pdf    = {https://leventebajczi.github.io/publications/tacas22.pdf},\\n    url_slides = {https://leventebajczi.github.io/publications/slides/tacas22.pdf},\\n    url_poster = {https://leventebajczi.github.io/publications/posters/tacas22.pdf},\\n\\turl_mtmt = {https://m2.mtmt.hu/api/publication/32801008},\\n}\\n\\n\\n\",\"author_short\":[\"Ádám, Z.\",\"Bajczi, L.\",\"Dobos-Kovács, M.\",\"Hajdu, Á.\",\"Molnár, V.\"],\"key\":\"MTMT:32801008\",\"id\":\"MTMT:32801008\",\"bibbaseid\":\"dm-bajczi-doboskovcs-hajdu-molnr-thetaportfolioofcegarbasedanalyseswithdynamicalgorithmselectioncompetitioncontribution-2022\",\"role\":\"author\",\"urls\":{\" pdf\":\"https://leventebajczi.github.io/publications/tacas22.pdf\",\" slides\":\"https://leventebajczi.github.io/publications/slides/tacas22.pdf\",\" poster\":\"https://leventebajczi.github.io/publications/posters/tacas22.pdf\",\" mtmt\":\"https://m2.mtmt.hu/api/publication/32801008\"},\"keyword\":[\"Computer Science\",\"Software Engineering\"],\"metadata\":{\"authorlinks\":{\"bajczi, l\":\"https://leventebajczi.com/publications.html\"}},\"downloads\":8,\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"inproceedings\",\"title\":\"ConcurrentWitness2Test: Test-Harnessing the Power of Concurrency (Competition Contribution)\",\"author\":[{\"propositions\":[],\"lastnames\":[\"Bajczi\"],\"firstnames\":[\"Levente\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Ádám\"],\"firstnames\":[\"Zsófia\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Micskei\"],\"firstnames\":[\"Zoltán\",\"Imre\"],\"suffixes\":[]}],\"booktitle\":\"Tools and Algorithms for the Construction and Analysis of Systems\",\"doi\":\"10.1007/978-3-031-57256-2_16\",\"unique-id\":\"34768972\",\"abstract\":\"ConcurrentWitness2Test is a violation witness validator for concurrent software. Taking both nondeterminism of data and interleaving-based nondeterminism into account, the tool aims to use the metadata described in the violation witnesses to synthesize an executable test harness. While plagued by some initial challenges yet to overcome, the validation performance of ConcurrentWitness2Test corroborates the usefulness of the proposed approach.\",\"year\":\"2024\",\"pages\":\"330-334\",\"orcid-numbers\":\"Bajczi, Levente/0000-0002-6551-5860; Ádám, Zsófia/0000-0003-2354-1750; Micskei, Zoltán Imre/0000-0003-1846-261X\",\"url_pdf\":\"https://leventebajczi.github.io/publications/tacas24cwt.pdf\",\"url_slides\":\"https://leventebajczi.github.io/publications/slides/tacas24cwt.pdf\",\"url_mtmt\":\"https://m2.mtmt.hu/api/publication/34768972\",\"bibtex\":\"@inproceedings{MTMT:34768972,\\n\\ttitle = {ConcurrentWitness2Test: Test-Harnessing the Power of Concurrency (Competition Contribution)},\\n\\tauthor = {Bajczi, Levente and Ádám, Zsófia and Micskei, Zoltán Imre},\\n\\tbooktitle = {Tools and Algorithms for the Construction and Analysis of Systems},\\n\\tdoi = {10.1007/978-3-031-57256-2_16},\\n\\tunique-id = {34768972},\\n\\tabstract = {ConcurrentWitness2Test is a violation witness validator for concurrent software. Taking both nondeterminism of data and interleaving-based nondeterminism into account, the tool aims to use the metadata described in the violation witnesses to synthesize an executable test harness. While plagued by some initial challenges yet to overcome, the validation performance of ConcurrentWitness2Test corroborates the usefulness of the proposed approach.},\\n\\tyear = {2024},\\n\\tpages = {330-334},\\n\\torcid-numbers = {Bajczi, Levente/0000-0002-6551-5860; Ádám, Zsófia/0000-0003-2354-1750; Micskei, Zoltán Imre/0000-0003-1846-261X},\\n\\n    url_pdf    = {https://leventebajczi.github.io/publications/tacas24cwt.pdf},\\n    url_slides = {https://leventebajczi.github.io/publications/slides/tacas24cwt.pdf},\\n    url_mtmt = {https://m2.mtmt.hu/api/publication/34768972},\\n}\\n\\n\",\"author_short\":[\"Bajczi, L.\",\"Ádám, Z.\",\"Micskei, Z. I.\"],\"key\":\"MTMT:34768972\",\"id\":\"MTMT:34768972\",\"bibbaseid\":\"bajczi-dm-micskei-concurrentwitness2testtestharnessingthepowerofconcurrencycompetitioncontribution-2024\",\"role\":\"author\",\"urls\":{\" pdf\":\"https://leventebajczi.github.io/publications/tacas24cwt.pdf\",\" slides\":\"https://leventebajczi.github.io/publications/slides/tacas24cwt.pdf\",\" mtmt\":\"https://m2.mtmt.hu/api/publication/34768972\"},\"metadata\":{\"authorlinks\":{\"bajczi, l\":\"https://leventebajczi.com/publications.html\"}},\"downloads\":2,\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"inproceedings\",\"title\":\"Theta: Abstraction Based Techniques for Verifying Concurrency (Competition Contribution)\",\"author\":[{\"propositions\":[],\"lastnames\":[\"Bajczi\"],\"firstnames\":[\"Levente\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Telbisz\"],\"firstnames\":[\"Csanád\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Somorjai\"],\"firstnames\":[\"Márk\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Ádám\"],\"firstnames\":[\"Zsófia\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Dobos-Kovács\"],\"firstnames\":[\"Mihály\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Szekeres\"],\"firstnames\":[\"Dániel\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Mondok\"],\"firstnames\":[\"Milán\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Molnár\"],\"firstnames\":[\"Vince\"],\"suffixes\":[]}],\"booktitle\":\"Tools and Algorithms for the Construction and Analysis of Systems\",\"doi\":\"10.1007/978-3-031-57256-2_30\",\"unique-id\":\"34768428\",\"abstract\":\"Theta is a model checking framework, with a strong emphasis on effectively handling concurrency in software using abstraction refinement algorithms. In SV-COMP 2024, we use 1) an abstraction-aware partial order reduction; 2) a dynamic statement reduction technique; and 3) enhanced support for call stacks to handle recursive programs. We integrate these techniques in an improved architecture with inherent support for portfolio-based verification using dynamic algorithm selection, with a diverse selection of supported SMT solvers as well. In this paper we detail the advances of Theta regarding concurrent and recursive software support.\",\"year\":\"2024\",\"pages\":\"412-417\",\"orcid-numbers\":\"Bajczi, Levente/0000-0002-6551-5860; Telbisz, Csanád/0000-0002-6260-5908; Ádám, Zsófia/0000-0003-2354-1750; Dobos-Kovács, Mihály/0000-0002-0064-2965; Szekeres, Dániel/0000-0002-2912-028X; Mondok, Milán/0000-0001-5396-2172; Molnár, Vince/0000-0002-8204-7595\",\"url_pdf\":\"https://leventebajczi.github.io/publications/tacas24theta.pdf\",\"url_slides\":\"https://leventebajczi.github.io/publications/slides/tacas24theta.pdf\",\"url_mtmt\":\"https://m2.mtmt.hu/api/publication/34768428\",\"bibtex\":\"@inproceedings{MTMT:34768428,\\n\\ttitle = {Theta: Abstraction Based Techniques for Verifying Concurrency (Competition Contribution)},\\n\\tauthor = {Bajczi, Levente and Telbisz, Csanád and Somorjai, Márk and Ádám, Zsófia and Dobos-Kovács, Mihály and Szekeres, Dániel and Mondok, Milán and Molnár, Vince},\\n\\tbooktitle = {Tools and Algorithms for the Construction and Analysis of Systems},\\n\\tdoi = {10.1007/978-3-031-57256-2_30},\\n\\tunique-id = {34768428},\\n\\tabstract = {Theta is a model checking framework, with a strong emphasis on effectively handling concurrency in software using abstraction refinement algorithms. In SV-COMP 2024, we use 1) an abstraction-aware partial order reduction; 2) a dynamic statement reduction technique; and 3) enhanced support for call stacks to handle recursive programs. We integrate these techniques in an improved architecture with inherent support for portfolio-based verification using dynamic algorithm selection, with a diverse selection of supported SMT solvers as well. In this paper we detail the advances of Theta regarding concurrent and recursive software support.},\\n\\tyear = {2024},\\n\\tpages = {412-417},\\n\\torcid-numbers = {Bajczi, Levente/0000-0002-6551-5860; Telbisz, Csanád/0000-0002-6260-5908; Ádám, Zsófia/0000-0003-2354-1750; Dobos-Kovács, Mihály/0000-0002-0064-2965; Szekeres, Dániel/0000-0002-2912-028X; Mondok, Milán/0000-0001-5396-2172; Molnár, Vince/0000-0002-8204-7595},\\n\\n    url_pdf    = {https://leventebajczi.github.io/publications/tacas24theta.pdf},\\n    url_slides = {https://leventebajczi.github.io/publications/slides/tacas24theta.pdf},\\n    url_mtmt = {https://m2.mtmt.hu/api/publication/34768428},\\n}\\n\\n\",\"author_short\":[\"Bajczi, L.\",\"Telbisz, C.\",\"Somorjai, M.\",\"Ádám, Z.\",\"Dobos-Kovács, M.\",\"Szekeres, D.\",\"Mondok, M.\",\"Molnár, V.\"],\"key\":\"MTMT:34768428\",\"id\":\"MTMT:34768428\",\"bibbaseid\":\"bajczi-telbisz-somorjai-dm-doboskovcs-szekeres-mondok-molnr-thetaabstractionbasedtechniquesforverifyingconcurrencycompetitioncontribution-2024\",\"role\":\"author\",\"urls\":{\" pdf\":\"https://leventebajczi.github.io/publications/tacas24theta.pdf\",\" slides\":\"https://leventebajczi.github.io/publications/slides/tacas24theta.pdf\",\" mtmt\":\"https://m2.mtmt.hu/api/publication/34768428\"},\"metadata\":{\"authorlinks\":{\"bajczi, l\":\"https://leventebajczi.com/publications.html\"}},\"downloads\":2,\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"inproceedings\",\"title\":\"EmergenTheta: Verification Beyond Abstraction Refinement (Competition Contribution)\",\"author\":[{\"propositions\":[],\"lastnames\":[\"Bajczi\"],\"firstnames\":[\"Levente\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Szekeres\"],\"firstnames\":[\"Dániel\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Mondok\"],\"firstnames\":[\"Milán\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Ádám\"],\"firstnames\":[\"Zsófia\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Somorjai\"],\"firstnames\":[\"Márk\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Telbisz\"],\"firstnames\":[\"Csanád\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Dobos-Kovács\"],\"firstnames\":[\"Mihály\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Molnár\"],\"firstnames\":[\"Vince\"],\"suffixes\":[]}],\"booktitle\":\"Tools and Algorithms for the Construction and Analysis of Systems\",\"doi\":\"10.1007/978-3-031-57256-2_23\",\"unique-id\":\"34768422\",\"abstract\":\"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.\",\"year\":\"2024\",\"pages\":\"371-375\",\"orcid-numbers\":\"Bajczi, Levente/0000-0002-6551-5860; Szekeres, Dániel/0000-0002-2912-028X; Mondok, Milán/0000-0001-5396-2172; Ádám, Zsófia/0000-0003-2354-1750; Telbisz, Csanád/0000-0002-6260-5908; Dobos-Kovács, Mihály/0000-0002-0064-2965; Molnár, Vince/0000-0002-8204-7595\",\"url_pdf\":\"https://leventebajczi.github.io/publications/tacas24etheta.pdf\",\"url_slides\":\"https://leventebajczi.github.io/publications/slides/tacas24etheta.pdf\",\"url_mtmt\":\"https://m2.mtmt.hu/api/publication/34768422\",\"bibtex\":\"@inproceedings{MTMT:34768422,\\n\\ttitle = {EmergenTheta: Verification Beyond Abstraction Refinement (Competition Contribution)},\\n\\tauthor = {Bajczi, Levente and Szekeres, Dániel and Mondok, Milán and Ádám, Zsófia and Somorjai, Márk and Telbisz, Csanád and Dobos-Kovács, Mihály and Molnár, Vince},\\n\\tbooktitle = {Tools and Algorithms for the Construction and Analysis of Systems},\\n\\tdoi = {10.1007/978-3-031-57256-2_23},\\n\\tunique-id = {34768422},\\n\\tabstract = {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.},\\n\\tyear = {2024},\\n\\tpages = {371-375},\\n\\torcid-numbers = {Bajczi, Levente/0000-0002-6551-5860; Szekeres, Dániel/0000-0002-2912-028X; Mondok, Milán/0000-0001-5396-2172; Ádám, Zsófia/0000-0003-2354-1750; Telbisz, Csanád/0000-0002-6260-5908; Dobos-Kovács, Mihály/0000-0002-0064-2965; Molnár, Vince/0000-0002-8204-7595},\\n\\n    url_pdf    = {https://leventebajczi.github.io/publications/tacas24etheta.pdf},\\n    url_slides = {https://leventebajczi.github.io/publications/slides/tacas24etheta.pdf},\\n    url_mtmt = {https://m2.mtmt.hu/api/publication/34768422},\\n}\\n\",\"author_short\":[\"Bajczi, L.\",\"Szekeres, D.\",\"Mondok, M.\",\"Ádám, Z.\",\"Somorjai, M.\",\"Telbisz, C.\",\"Dobos-Kovács, M.\",\"Molnár, V.\"],\"key\":\"MTMT:34768422\",\"id\":\"MTMT:34768422\",\"bibbaseid\":\"bajczi-szekeres-mondok-dm-somorjai-telbisz-doboskovcs-molnr-emergenthetaverificationbeyondabstractionrefinementcompetitioncontribution-2024\",\"role\":\"author\",\"urls\":{\" pdf\":\"https://leventebajczi.github.io/publications/tacas24etheta.pdf\",\" slides\":\"https://leventebajczi.github.io/publications/slides/tacas24etheta.pdf\",\" mtmt\":\"https://m2.mtmt.hu/api/publication/34768422\"},\"metadata\":{\"authorlinks\":{\"bajczi, l\":\"https://leventebajczi.com/publications.html\"}},\"downloads\":1,\"html\":\"\"}],\n      metadata: {\"owner\":\"bajczi, l\",\"authorlinks\":{\"bajczi, l\":\"https://leventebajczi.com/publications.html\"}},\n      ownerID: \"GynLprJytscbSLvgL\"\n    };\n  </script>\n\n  <script type=\"text/javascript\">\n  var site$;\n  if (typeof $ != 'undefined') {\n    console.log('existing jquery: storing and then restoring');\n    site$ = $;\n    $ = null;\n  }\n  </script>\n\n  <script src=\"https://ajax.googleapis.com/ajax/libs/jquery/2.2.4/jquery.min.js\">\n  </script>\n  <script type=\"text/javascript\">\n  if (site$) {\n    console.log('existing jquery: avoiding conflict and restoring');\n    bb$ = $.noConflict(true);\n    $ = site$;\n  } else {\n    bb$ = $;\n  }\n  </script>\n\n  <script src=\"//bibbase.org/js/bibbase.min.js\"\n          type=\"text/javascript\">\n  </script>\n\n  <script type=\"text/javascript\"\n          src=\"https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.1/MathJax.js?config=TeX-AMS-MML_HTMLorMML\">\n  </script>\n  <script type=\"text/x-mathjax-config\">\n    MathJax.Hub.Config({tex2jax: {inlineMath: [['$','$'], ['\\\\(','\\\\)']]},\n                        skipTags: [\"body\"],\n                        processClass: \"bibbase_paper\"});\n  </script>\n\n  <style>\n  @media print {\n    .dontprint {\n        display: none !important;\n    }\n\n  .bibbase_group {\n    background-color: #E0E0E0;\n    font-style: italic;\n    font-size: larger;\n    text-shadow: 0px 0px 3px #FFFFFF;\n    border-radius: 4px 4px 4px 4px;\n    -moz-border-radius: 4px 4px 4px 4px;\n    -webkit-border-radius: 4px;\n    padding: 5px 40px 5px;\n    margin-top: 10px;\n    margin-bottom: 5px;\n    cursor: pointer;\n  }\n\n  .bibbase_paper {\n    margin-bottom: 5px;\n  }\n\n  }\n  </style>\n\n  \n  <div style=\"float: right; margin-right: 10px; margin-top: 10px; text-align: right; font-size: 12px\">\n    generated by\n    <a href=\"//bibbase.org\"\n       onclick=\"trackOutboundLink('bibbase', 'logo clicked', window.location.href, '//bibbase.org'); return false;\">\n      <img src=\"//bibbase.org/img/logo.svg\"\n           style=\"vertical-align: middle; margin-left: 3px; height: 16px;\"/\n           alt=\"bibbase.org\"\n           title=\"BibBase – The easiest way to maintain your publications page.\"\n        ></a>\n    \n  </div>\n  \n\n  <div id=\"bibbase_header\" class=\"dontprint\" style=\"\">\n\n    <ul class=\"nav nav-pills\" style=\"margin: 0px;\">\n\n      <li class=\"dropdown\" id=\"groupby_dropdown\">\n      <a class=\"dropdown-toggle\"\n         data-toggle=\"dropdown\"\n         href=\"#\">\n          Group by\n          <b class=\"caret\"></b>\n      </a>\n      <ul class=\"dropdown-menu\">\n        <li class=\"groupby year\"><a onclick=\"groupby('year')\">\n            Year</a>\n        </li>\n        <li class=\"groupby author\"><a onclick=\"groupby('author_short')\">\n            Author</a>\n        </li>\n        <li class=\"groupby type\"><a onclick=\"groupby('type')\">\n            Type</a>\n        </li>\n        <li class=\"groupby keyword\"><a onclick=\"groupby('keyword')\">\n            Keyword</a>\n        </li>\n        <li class=\"groupby downloads\"><a onclick=\"groupby('downloads')\">\n            Downloads</a>\n        </li>\n      </ul>\n      </li>\n\n\n      <li class=\"dropdown\" id=\"menu_dropdown\">\n      <a class=\"dropdown-toggle\"\n         data-toggle=\"dropdown\"\n         href=\"#\" alt=\"controls\">\n          <i class=\"fa fa-reorder\" alt=\"controls\"></i>\n          <b class=\"caret\"></b>\n      </a>\n      <ul class=\"dropdown-menu\">\n        <li>\n          <a onclick=\"toggleAll()\">\n            <i class=\"fa fa-chevron-down fa-fw\"></i> Expand/Collapse All\n          </a>\n        </li>\n        <li>\n          <a download=\"publications.bib\" href=\"data:text/bibtex;base64,QGlucHJvY2VlZGluZ3N7TVRNVDozMjgzNjU4MywKCXRpdGxlID0ge0MgZm9yIFlvdXJzZWxmOiBDb21wYXJpc29uIG9mIEZyb250LUVuZCBUZWNobmlxdWVzIGZvciBGb3JtYWwgVmVyaWZpY2F0aW9ufSwKCWF1dGhvciA9IHtCYWpjemksIExldmVudGUgYW5kIMOBZMOhbSwgWnPDs2ZpYSBhbmQgTW9sbsOhciwgVmluY2V9LAoJYm9va3RpdGxlID0gezIwMjIgSUVFRS9BQ00gMTB0aCBJbnRlcm5hdGlvbmFsIENvbmZlcmVuY2Ugb24gRm9ybWFsIE1ldGhvZHMgaW4gU29mdHdhcmUgRW5naW5lZXJpbmcgKEZvcm1hbGlTRSl9LAoJZG9pID0gezEwLjExNDUvMzUyNDQ4Mi4zNTI3NjQ2fSwKCXVuaXF1ZS1pZCA9IHszMjgzNjU4M30sCgl5ZWFyID0gezIwMjJ9LAoJb3JjaWQtbnVtYmVycyA9IHtCYWpjemksIExldmVudGUvMDAwMC0wMDAyLTY1NTEtNTg2MDsgw4Fkw6FtLCBac8OzZmlhLzAwMDAtMDAwMy0yMzU0LTE3NTA7IE1vbG7DoXIsIFZpbmNlLzAwMDAtMDAwMi04MjA0LTc1OTV9LAoJYWJzdHJhY3QgPSB7V2l0aCB0aGUgaW1wcm92ZW1lbnQgb2YgaGFyZHdhcmUgYW5kIGFsZ29yaXRobXMsIHRoZSBtYWluIGNoYWxsZW5nZSBvZiBzb2Z0d2FyZSBtb2RlbCBjaGVja2luZyBoYXMgc2hpZnRlZCBmcm9tIHB1cmUgYWxnb3JpdGhtaWMgcGVyZm9ybWFuY2UgdG93YXJkIHN1cHBvcnRpbmcgYSB3aWRlciBzZXQgb2YgaW5wdXQgcHJvZ3JhbXMuIFN1Y2Nlc3NmdWwgdG9vbGNoYWlucyB0YWNrbGUgdGhlIHByb2JsZW0gb2YgcGFyc2luZyBhIHdpZGUgcmFuZ2Ugb2YgaW5wdXRzIGluIGFuIGVmZmljaWVudCB3YXkgYnkgcmV1c2luZyBzb2x1dGlvbnMgZnJvbSBleGlzdGluZyBjb21waWxlciB0ZWNobm9sb2dpZXMgc3VjaCBhcyBFY2xpcHNlIENEVCBvciBMTFZNLiBPdXIgZXhwZXJpZW5jZSBzdWdnZXN0cyB0aGF0IHdlbGwtZXN0YWJsaXNoZWQgdGVjaG5pcXVlcyBpbiBjb21waWxlciB0ZWNobm9sb2d5IGFyZSBub3QgbmVjZXNzYXJpbHkgYmVuZWZpY2lhbCB0byBtb2RlbCBjaGVja2VycyBhbmQgc29tZXRpbWVzIGNhbiBldmVuIGh1cnQgdGhlaXIgcGVyZm9ybWFuY2UuIEluIHRoaXMgcGFwZXIsIHdlIHJldmlldyB0aGUgdG9vbHMgbWF0dXJlIGVub3VnaCB0byBwYXJ0aWNpcGF0ZSBpbiB0aGUgU29mdHdhcmUgVmVyaWZpY2F0aW9uIENvbXBldGl0aW9uIGluIHRlcm1zIG9mIHRoZSBlbXBsb3llZCBhbmFseXNpcyBhbmQgZnJvbnRlbmQgdGVjaG5pcXVlcy4gV2UgZmluZCB0aGF0IHN1Y2Nlc3NmdWwgdG9vbHMgZG8gZXhoaWJpdCBhIGJpYXMgdG93YXJkIGNlcnRhaW4gY29tYmluYXRpb25zLiBXZSBleHBsb3JlIHRoZSB0aGVvcmV0aWNhbCByZWFzb25zIGFuZCBzdWdnZXN0IGFuIGFkYXB0YWJsZSBhcHByb2FjaCBmb3IgbW9kZWwgY2hlY2tpbmcgZnJhbWV3b3Jrcy4gV2UgdmFsaWRhdGUgb3VyIHJlY29tbWVuZGF0aW9ucyBieSBpbXBsZW1lbnRpbmcgYSBuZXcgZnJvbnRlbmQgZm9yIGEgbW9kZWwgY2hlY2tpbmcgZnJhbWV3b3JrIGFuZCBzaG93IHRoYXQgaXQgaW5kZWVkIGJlbmVmaXRzIHNvbWUgb2YgdGhlIGFsZ29yaXRobXMufSwKCiAgICB1cmxfcGRmICAgID0ge2h0dHBzOi8vbGV2ZW50ZWJhamN6aS5naXRodWIuaW8vcHVibGljYXRpb25zL2Zvcm1hbGlzZTIyLnBkZn0sCiAgICB1cmxfc2xpZGVzID0ge2h0dHBzOi8vbGV2ZW50ZWJhamN6aS5naXRodWIuaW8vcHVibGljYXRpb25zL3NsaWRlcy9mb3JtYWxpc2UyMi5wZGZ9LAoJdXJsX210bXQgPSB7aHR0cHM6Ly9tMi5tdG10Lmh1L2FwaS9wdWJsaWNhdGlvbi8zMjgzNjU4M30sCn0KCgoKQGFydGljbGV7TVRNVDozMDg2NTUxNSwKCXRpdGxlID0ge1dpbGwgTXkgUHJvZ3JhbSBCcmVhayBvbiBUaGlzIEZhdWx0eSBQcm9jZXNzb3I/LiBGb3JtYWwgQW5hbHlzaXMgb2YgSGFyZHdhcmUgRmF1bHQgQWN0aXZhdGlvbnMgaW4gQ29uY3VycmVudCBFbWJlZGRlZCBTb2Z0d2FyZX0sCglhdXRob3IgPSB7QmFqY3ppLCBMZXZlbnRlIGFuZCBWw7Zyw7ZzLCBBbmRyw6FzIGFuZCBNb2xuw6FyLCBWaW5jZX0sCglkb2kgPSB7MTAuMTE0NS8zMzU4MjM4fSwKCWpvdXJuYWwtaXNvID0ge0FDTSBUIEVNQkVEIENPTVBVVCBTfSwKCWpvdXJuYWwgPSB7QUNNIFRSQU5TQUNUSU9OUyBPTiBFTUJFRERFRCBDT01QVVRJTkcgU1lTVEVNU30sCgl2b2x1bWUgPSB7MTh9LAoJdW5pcXVlLWlkID0gezMwODY1NTE1fSwKCWlzc24gPSB7MTUzOS05MDg3fSwKCWFic3RyYWN0ID0ge0Zvcm1hbCB2ZXJpZmljYXRpb24gaXMgYXBwcm9hY2hpbmcgYSBwb2ludCB3aGVyZSBpdCB3aWxsIGJlIHJlbGlhYmx5IGFwcGxpY2FibGUgdG8gZW1iZWRkZWQgc29mdHdhcmUuIEV2ZW4gdGhvdWdoIGZvcm1hbCB2ZXJpZmljYXRpb24gY2FuIGVmZmljaWVudGx5IGFuYWx5emUgbXVsdGktdGhyZWFkZWQgYXBwbGljYXRpb25zLCBtdWx0aS1jb3JlIHByb2Nlc3NvcnMgYXJlIG9mdGVuIGNvbnNpZGVyZWQgdG9vIGRhbmdlcm91cyB0byB1c2UgaW4gY3JpdGljYWwgc3lzdGVtcywgZGVzcGl0ZSB0aGUgbWFueSBiZW5lZml0cyB0aGV5IGNhbiBvZmZlci4gT25lIHJlYXNvbiBpcyB0aGUgYWR2YW5jZWQgbWVtb3J5IGNvbnNpc3RlbmN5IG1vZGVsIG9mIHN1Y2ggQ1BVcy4gTm93YWRheXMsIG1vc3Qgc29mdHdhcmUgdmVyaWZpZXJzIGFzc3VtZSBzdHJpY3Qgc2VxdWVudGlhbCBjb25zaXN0ZW5jeSwgd2hpY2ggaXMgYWxzbyB0aGUgbmHDr3ZlIHZpZXcgb2YgcHJvZ3JhbW1lcnMuIE1vZGVybiBtdWx0aS1jb3JlIHByb2Nlc3NvcnMsIGhvd2V2ZXIsIHJhcmVseSBndWFyYW50ZWUgdGhpcyBhc3N1bXB0aW9uIGJ5IGRlZmF1bHQuIEluIGFkZGl0aW9uLCBjb21wbGV4IHByb2Nlc3NvciBhcmNoaXRlY3R1cmVzIG1heSBlYXNpbHkgY29udGFpbiBkZXNpZ24gZmF1bHRzLiBUaGFua3MgdG8gdGhlIHJlY2VudCBhZHZhbmNlcyBpbiBoYXJkd2FyZSB2ZXJpZmljYXRpb24sIHRoZXNlIGZhdWx0cyBhcmUgaW5jcmVhc2luZ2x5IHZpc2libGUgYW5kIGNhbiBiZSBkZXRlY3RlZCBldmVuIGluIGV4aXN0aW5nIHByb2Nlc3NvcnMsIGdpdmluZyBhbiBvcHBvcnR1bml0eSB0byBjb21wZW5zYXRlIGZvciB0aGUgcHJvYmxlbSBpbiBzb2Z0d2FyZS4gSW4gdGhpcyBwYXBlciwgd2UgcHJvcG9zZSBhIGdlbmVyaWMgYXBwcm9hY2ggdG8gY29uc2lkZXIgaW5jb25zaXN0ZW50IGJlaGF2aW9yIG9mIHRoZSBoYXJkd2FyZSBpbiB0aGUgYW5hbHlzaXMgb2Ygc29mdHdhcmUuIE91ciBhcHByb2FjaCBpcyBiYXNlZCBvbiBmb3JtYWwgbWV0aG9kcyBhbmQgY2FuIGJlIHVzZWQgdG8gZGV0ZWN0IHRoZSBhY3RpdmF0aW9uIG9mIGV4aXN0aW5nIGhhcmR3YXJlIGZhdWx0cyBvbiB0aGUgYXBwbGljYXRpb24gbGV2ZWwgYW5kIGZhY2lsaXRhdGUgdGhlaXIgbWl0aWdhdGlvbiBpbiBzb2Z0d2FyZS4gVGhlIGFwcHJvYWNoIHJlbGllcyBoZWF2aWx5IG9uIHJlY2VudCByZXN1bHRzIG9mIG1vZGVsIGNoZWNraW5nIGFuZCBoYXJkd2FyZSB2ZXJpZmljYXRpb24gYW5kIG9mZmVycyBuZXcsIGludGVncmF0aXZlIHJlc2VhcmNoIGRpcmVjdGlvbnMuIFdlIHByb3Bvc2UgYSBwYXJ0aWFsIHNvbHV0aW9uIGJhc2VkIG9uIGV4aXN0aW5nIG1vZGVsIGNoZWNraW5nIHRvb2xzIHRvIGRlbW9uc3RyYXRlIGZlYXNpYmlsaXR5IGFuZCBldmFsdWF0ZSB0aGVpciBwZXJmb3JtYW5jZSBpbiB0aGlzIGNvbnRleHQufSwKCXllYXIgPSB7MjAxOX0sCgllaXNzbiA9IHsxNTU4LTM0NjV9LAoJb3JjaWQtbnVtYmVycyA9IHtCYWpjemksIExldmVudGUvMDAwMC0wMDAyLTY1NTEtNTg2MDsgTW9sbsOhciwgVmluY2UvMDAwMC0wMDAyLTgyMDQtNzU5NX0sCgogICAgdXJsX3BkZiAgICA9IHtodHRwczovL2xldmVudGViYWpjemkuZ2l0aHViLmlvL3B1YmxpY2F0aW9ucy9lbXNvZnQxOS5wZGZ9LAogICAgdXJsX3NsaWRlcyA9IHtodHRwczovL2xldmVudGViYWpjemkuZ2l0aHViLmlvL3B1YmxpY2F0aW9ucy9zbGlkZXMvZW1zb2Z0MTkucGRmfSwKCXVybF9tdG10ID0ge2h0dHBzOi8vbTIubXRtdC5odS9hcGkvcHVibGljYXRpb24vMzA4NjU1MTV9LAkKfQoKCgpAYXJ0aWNsZXtNVE1UOjMyODAxMDA4LAoJdGl0bGUgPSB7VGhldGE6IHBvcnRmb2xpbyBvZiBDRUdBUi1iYXNlZCBhbmFseXNlcyB3aXRoIGR5bmFtaWMgYWxnb3JpdGhtIHNlbGVjdGlvbiAoQ29tcGV0aXRpb24gQ29udHJpYnV0aW9uKX0sCglhdXRob3IgPSB7w4Fkw6FtLCBac8OzZmlhIGFuZCBCYWpjemksIExldmVudGUgYW5kIERvYm9zLUtvdsOhY3MsIE1paMOhbHkgYW5kIEhhamR1LCDDgWtvcyBhbmQgTW9sbsOhciwgVmluY2V9LAoJZG9pID0gezEwLjEwMDcvOTc4LTMtMDMwLTk5NTI3LTBfMzR9LAoJam91cm5hbC1pc28gPSB7TEVDVCBOT1RFUyBDT01QVVQgU0N9LAoJam91cm5hbCA9IHtMRUNUVVJFIE5PVEVTIElOIENPTVBVVEVSIFNDSUVOQ0V9LAoJdm9sdW1lID0gezEzMjQ0fSwKCXVuaXF1ZS1pZCA9IHszMjgwMTAwOH0sCglpc3NuID0gezAzMDItOTc0M30sCglrZXl3b3JkcyA9IHtDb21wdXRlciBTY2llbmNlLCBTb2Z0d2FyZSBFbmdpbmVlcmluZ30sCgl5ZWFyID0gezIwMjJ9LAoJZWlzc24gPSB7MTYxMS0zMzQ5fSwKCXBhZ2VzID0gezQ3NC00Nzh9LAoJb3JjaWQtbnVtYmVycyA9IHvDgWTDoW0sIFpzw7NmaWEvMDAwMC0wMDAzLTIzNTQtMTc1MDsgQmFqY3ppLCBMZXZlbnRlLzAwMDAtMDAwMi02NTUxLTU4NjA7IERvYm9zLUtvdsOhY3MsIE1paMOhbHkvMDAwMC0wMDAyLTAwNjQtMjk2NTsgSGFqZHUsIMOBa29zLzAwMDAtMDAwMS04MDAxLTg4NjU7IE1vbG7DoXIsIFZpbmNlLzAwMDAtMDAwMi04MjA0LTc1OTV9LAoJYWJzdHJhY3QgPSB7VEhFVEEgaXMgYSBtb2RlbCBjaGVja2luZyBmcmFtZXdvcmsgYmFzZWQgb24gYWJzdHJhY3Rpb24gcmVmaW5lbWVudCBhbGdvcml0aG1zLiBJbiBTVi1DT01QIDIwMjIsIHdlIGludHJvZHVjZTogMSkgcmVhc29uaW5nIGF0IHRoZSBzb3VyY2UtbGV2ZWwgdmlhIGEgZGlyZWN0IHRyYW5zbGF0aW9uIGZyb20gQyBwcm9ncmFtczsgMikgc3VwcG9ydCBmb3IgY29uY3VycmVudCBwcm9ncmFtcyB3aXRoIGludGVybGVhdmluZyBzZW1hbnRpY3M7IDMpIG1pdGlnYXRpb24gZm9yIG5vbi1wcm9ncmVzc2luZyByZWZpbmVtZW50IGxvb3BzOyA0KSBzdXBwb3J0IGZvciBTTVQtTElCLWNvbXBsaWFudCBzb2x2ZXJzLiBXZSBjb21iaW5lIGFsbCBvZiB0aGUgYWZvcmVtZW50aW9uZWQgdGVjaG5pcXVlcyBpbnRvIGEgcG9ydGZvbGlvIHdpdGggZHluYW1pYyBhbGdvcml0aG0gc2VsZWN0aW9uLn0sCgogICAgdXJsX3BkZiAgICA9IHtodHRwczovL2xldmVudGViYWpjemkuZ2l0aHViLmlvL3B1YmxpY2F0aW9ucy90YWNhczIyLnBkZn0sCiAgICB1cmxfc2xpZGVzID0ge2h0dHBzOi8vbGV2ZW50ZWJhamN6aS5naXRodWIuaW8vcHVibGljYXRpb25zL3NsaWRlcy90YWNhczIyLnBkZn0sCiAgICB1cmxfcG9zdGVyID0ge2h0dHBzOi8vbGV2ZW50ZWJhamN6aS5naXRodWIuaW8vcHVibGljYXRpb25zL3Bvc3RlcnMvdGFjYXMyMi5wZGZ9LAoJdXJsX210bXQgPSB7aHR0cHM6Ly9tMi5tdG10Lmh1L2FwaS9wdWJsaWNhdGlvbi8zMjgwMTAwOH0sCn0KCgoKCkBpbnByb2NlZWRpbmdze01UTVQ6MzQ3Njg5NzIsCgl0aXRsZSA9IHtDb25jdXJyZW50V2l0bmVzczJUZXN0OiBUZXN0LUhhcm5lc3NpbmcgdGhlIFBvd2VyIG9mIENvbmN1cnJlbmN5IChDb21wZXRpdGlvbiBDb250cmlidXRpb24pfSwKCWF1dGhvciA9IHtCYWpjemksIExldmVudGUgYW5kIMOBZMOhbSwgWnPDs2ZpYSBhbmQgTWljc2tlaSwgWm9sdMOhbiBJbXJlfSwKCWJvb2t0aXRsZSA9IHtUb29scyBhbmQgQWxnb3JpdGhtcyBmb3IgdGhlIENvbnN0cnVjdGlvbiBhbmQgQW5hbHlzaXMgb2YgU3lzdGVtc30sCglkb2kgPSB7MTAuMTAwNy85NzgtMy0wMzEtNTcyNTYtMl8xNn0sCgl1bmlxdWUtaWQgPSB7MzQ3Njg5NzJ9LAoJYWJzdHJhY3QgPSB7Q29uY3VycmVudFdpdG5lc3MyVGVzdCBpcyBhIHZpb2xhdGlvbiB3aXRuZXNzIHZhbGlkYXRvciBmb3IgY29uY3VycmVudCBzb2Z0d2FyZS4gVGFraW5nIGJvdGggbm9uZGV0ZXJtaW5pc20gb2YgZGF0YSBhbmQgaW50ZXJsZWF2aW5nLWJhc2VkIG5vbmRldGVybWluaXNtIGludG8gYWNjb3VudCwgdGhlIHRvb2wgYWltcyB0byB1c2UgdGhlIG1ldGFkYXRhIGRlc2NyaWJlZCBpbiB0aGUgdmlvbGF0aW9uIHdpdG5lc3NlcyB0byBzeW50aGVzaXplIGFuIGV4ZWN1dGFibGUgdGVzdCBoYXJuZXNzLiBXaGlsZSBwbGFndWVkIGJ5IHNvbWUgaW5pdGlhbCBjaGFsbGVuZ2VzIHlldCB0byBvdmVyY29tZSwgdGhlIHZhbGlkYXRpb24gcGVyZm9ybWFuY2Ugb2YgQ29uY3VycmVudFdpdG5lc3MyVGVzdCBjb3Jyb2JvcmF0ZXMgdGhlIHVzZWZ1bG5lc3Mgb2YgdGhlIHByb3Bvc2VkIGFwcHJvYWNoLn0sCgl5ZWFyID0gezIwMjR9LAoJcGFnZXMgPSB7MzMwLTMzNH0sCglvcmNpZC1udW1iZXJzID0ge0JhamN6aSwgTGV2ZW50ZS8wMDAwLTAwMDItNjU1MS01ODYwOyDDgWTDoW0sIFpzw7NmaWEvMDAwMC0wMDAzLTIzNTQtMTc1MDsgTWljc2tlaSwgWm9sdMOhbiBJbXJlLzAwMDAtMDAwMy0xODQ2LTI2MVh9LAoKICAgIHVybF9wZGYgICAgPSB7aHR0cHM6Ly9sZXZlbnRlYmFqY3ppLmdpdGh1Yi5pby9wdWJsaWNhdGlvbnMvdGFjYXMyNGN3dC5wZGZ9LAogICAgdXJsX3NsaWRlcyA9IHtodHRwczovL2xldmVudGViYWpjemkuZ2l0aHViLmlvL3B1YmxpY2F0aW9ucy9zbGlkZXMvdGFjYXMyNGN3dC5wZGZ9LAogICAgdXJsX210bXQgPSB7aHR0cHM6Ly9tMi5tdG10Lmh1L2FwaS9wdWJsaWNhdGlvbi8zNDc2ODk3Mn0sCn0KCgoKQGlucHJvY2VlZGluZ3N7TVRNVDozNDc2ODQyOCwKCXRpdGxlID0ge1RoZXRhOiBBYnN0cmFjdGlvbiBCYXNlZCBUZWNobmlxdWVzIGZvciBWZXJpZnlpbmcgQ29uY3VycmVuY3kgKENvbXBldGl0aW9uIENvbnRyaWJ1dGlvbil9LAoJYXV0aG9yID0ge0JhamN6aSwgTGV2ZW50ZSBhbmQgVGVsYmlzeiwgQ3NhbsOhZCBhbmQgU29tb3JqYWksIE3DoXJrIGFuZCDDgWTDoW0sIFpzw7NmaWEgYW5kIERvYm9zLUtvdsOhY3MsIE1paMOhbHkgYW5kIFN6ZWtlcmVzLCBEw6FuaWVsIGFuZCBNb25kb2ssIE1pbMOhbiBhbmQgTW9sbsOhciwgVmluY2V9LAoJYm9va3RpdGxlID0ge1Rvb2xzIGFuZCBBbGdvcml0aG1zIGZvciB0aGUgQ29uc3RydWN0aW9uIGFuZCBBbmFseXNpcyBvZiBTeXN0ZW1zfSwKCWRvaSA9IHsxMC4xMDA3Lzk3OC0zLTAzMS01NzI1Ni0yXzMwfSwKCXVuaXF1ZS1pZCA9IHszNDc2ODQyOH0sCglhYnN0cmFjdCA9IHtUaGV0YSBpcyBhIG1vZGVsIGNoZWNraW5nIGZyYW1ld29yaywgd2l0aCBhIHN0cm9uZyBlbXBoYXNpcyBvbiBlZmZlY3RpdmVseSBoYW5kbGluZyBjb25jdXJyZW5jeSBpbiBzb2Z0d2FyZSB1c2luZyBhYnN0cmFjdGlvbiByZWZpbmVtZW50IGFsZ29yaXRobXMuIEluIFNWLUNPTVAgMjAyNCwgd2UgdXNlIDEpIGFuIGFic3RyYWN0aW9uLWF3YXJlIHBhcnRpYWwgb3JkZXIgcmVkdWN0aW9uOyAyKSBhIGR5bmFtaWMgc3RhdGVtZW50IHJlZHVjdGlvbiB0ZWNobmlxdWU7IGFuZCAzKSBlbmhhbmNlZCBzdXBwb3J0IGZvciBjYWxsIHN0YWNrcyB0byBoYW5kbGUgcmVjdXJzaXZlIHByb2dyYW1zLiBXZSBpbnRlZ3JhdGUgdGhlc2UgdGVjaG5pcXVlcyBpbiBhbiBpbXByb3ZlZCBhcmNoaXRlY3R1cmUgd2l0aCBpbmhlcmVudCBzdXBwb3J0IGZvciBwb3J0Zm9saW8tYmFzZWQgdmVyaWZpY2F0aW9uIHVzaW5nIGR5bmFtaWMgYWxnb3JpdGhtIHNlbGVjdGlvbiwgd2l0aCBhIGRpdmVyc2Ugc2VsZWN0aW9uIG9mIHN1cHBvcnRlZCBTTVQgc29sdmVycyBhcyB3ZWxsLiBJbiB0aGlzIHBhcGVyIHdlIGRldGFpbCB0aGUgYWR2YW5jZXMgb2YgVGhldGEgcmVnYXJkaW5nIGNvbmN1cnJlbnQgYW5kIHJlY3Vyc2l2ZSBzb2Z0d2FyZSBzdXBwb3J0Ln0sCgl5ZWFyID0gezIwMjR9LAoJcGFnZXMgPSB7NDEyLTQxN30sCglvcmNpZC1udW1iZXJzID0ge0JhamN6aSwgTGV2ZW50ZS8wMDAwLTAwMDItNjU1MS01ODYwOyBUZWxiaXN6LCBDc2Fuw6FkLzAwMDAtMDAwMi02MjYwLTU5MDg7IMOBZMOhbSwgWnPDs2ZpYS8wMDAwLTAwMDMtMjM1NC0xNzUwOyBEb2Jvcy1Lb3bDoWNzLCBNaWjDoWx5LzAwMDAtMDAwMi0wMDY0LTI5NjU7IFN6ZWtlcmVzLCBEw6FuaWVsLzAwMDAtMDAwMi0yOTEyLTAyOFg7IE1vbmRvaywgTWlsw6FuLzAwMDAtMDAwMS01Mzk2LTIxNzI7IE1vbG7DoXIsIFZpbmNlLzAwMDAtMDAwMi04MjA0LTc1OTV9LAoKICAgIHVybF9wZGYgICAgPSB7aHR0cHM6Ly9sZXZlbnRlYmFqY3ppLmdpdGh1Yi5pby9wdWJsaWNhdGlvbnMvdGFjYXMyNHRoZXRhLnBkZn0sCiAgICB1cmxfc2xpZGVzID0ge2h0dHBzOi8vbGV2ZW50ZWJhamN6aS5naXRodWIuaW8vcHVibGljYXRpb25zL3NsaWRlcy90YWNhczI0dGhldGEucGRmfSwKICAgIHVybF9tdG10ID0ge2h0dHBzOi8vbTIubXRtdC5odS9hcGkvcHVibGljYXRpb24vMzQ3Njg0Mjh9LAp9CgoKCkBpbnByb2NlZWRpbmdze01UTVQ6MzQ3Njg0MjIsCgl0aXRsZSA9IHtFbWVyZ2VuVGhldGE6IFZlcmlmaWNhdGlvbiBCZXlvbmQgQWJzdHJhY3Rpb24gUmVmaW5lbWVudCAoQ29tcGV0aXRpb24gQ29udHJpYnV0aW9uKX0sCglhdXRob3IgPSB7QmFqY3ppLCBMZXZlbnRlIGFuZCBTemVrZXJlcywgRMOhbmllbCBhbmQgTW9uZG9rLCBNaWzDoW4gYW5kIMOBZMOhbSwgWnPDs2ZpYSBhbmQgU29tb3JqYWksIE3DoXJrIGFuZCBUZWxiaXN6LCBDc2Fuw6FkIGFuZCBEb2Jvcy1Lb3bDoWNzLCBNaWjDoWx5IGFuZCBNb2xuw6FyLCBWaW5jZX0sCglib29rdGl0bGUgPSB7VG9vbHMgYW5kIEFsZ29yaXRobXMgZm9yIHRoZSBDb25zdHJ1Y3Rpb24gYW5kIEFuYWx5c2lzIG9mIFN5c3RlbXN9LAoJZG9pID0gezEwLjEwMDcvOTc4LTMtMDMxLTU3MjU2LTJfMjN9LAoJdW5pcXVlLWlkID0gezM0NzY4NDIyfSwKCWFic3RyYWN0ID0ge1RoZXRhIGlzIGEgbW9kZWwgY2hlY2tpbmcgZnJhbWV3b3JrIGNvbnZlbnRpb25hbGx5IGJhc2VkIG9uIGFic3RyYWN0aW9uIHJlZmluZW1lbnQgdGVjaG5pcXVlcy4gV2hpbGUgYWJzdHJhY3Rpb24gaXMgdXNlZnVsIGZvciBhIGxhcmdlIG51bWJlciBvZiB2ZXJpZmljYXRpb24gcHJvYmxlbXMsIHRoZSBvdmVyLXJlbGlhbmNlIG9uIHRoZSB0ZWNobmlxdWUgbGVkIHRvIFRoZXRhIGJlaW5nIHVuYWJsZSB0byBtZWFuaW5nZnVsbHkgYWRhcHQuIElkZW50aWZ5aW5nIHRoaXMgcHJvYmxlbSBpbiBwcmV2aW91cyB5ZWFycyBvZiBTVi1DT01QIGhhcyBsZWQgdXMgdG8gY3JlYXRlIEVtZXJnZW5UaGV0YSAsIGEgc2FuZGJveCBmb3IgdGhlIG5ldyBhcHByb2FjaGVzIHdlIHdhbnQgVGhldGEgdG8gc3VwcG9ydC4gQnkgZGlmZmVyZW50aWF0aW5nIGJldHdlZW4gbWF0dXJlIGFuZCBlbWVyZ2luZyB0ZWNobmlxdWVzLCB3ZSBjYW4gZXhwZXJpbWVudCBtb3JlIGZyZWVseSB3aXRob3V0IGh1cnRpbmcgdGhlIHJlbGlhYmlsaXR5IG9mIHRoZSBvdmVyYWxsIGZyYW1ld29yay4gSW4gdGhpcyBwYXBlciB3ZSBkZXRhaWwgdGhlIGRldmVsb3BtZW50IHJvdXRlIHRvIEVtZXJnZW5UaGV0YSAsIGFuZCBpdHMgZmlyc3QgZGVidXQgb24gU1YtQ09NUOKAmTI0IGluIHRoZSBSZWFjaFNhZmV0eSBjYXRlZ29yeS59LAoJeWVhciA9IHsyMDI0fSwKCXBhZ2VzID0gezM3MS0zNzV9LAoJb3JjaWQtbnVtYmVycyA9IHtCYWpjemksIExldmVudGUvMDAwMC0wMDAyLTY1NTEtNTg2MDsgU3pla2VyZXMsIETDoW5pZWwvMDAwMC0wMDAyLTI5MTItMDI4WDsgTW9uZG9rLCBNaWzDoW4vMDAwMC0wMDAxLTUzOTYtMjE3Mjsgw4Fkw6FtLCBac8OzZmlhLzAwMDAtMDAwMy0yMzU0LTE3NTA7IFRlbGJpc3osIENzYW7DoWQvMDAwMC0wMDAyLTYyNjAtNTkwODsgRG9ib3MtS292w6FjcywgTWlow6FseS8wMDAwLTAwMDItMDA2NC0yOTY1OyBNb2xuw6FyLCBWaW5jZS8wMDAwLTAwMDItODIwNC03NTk1fSwKCiAgICB1cmxfcGRmICAgID0ge2h0dHBzOi8vbGV2ZW50ZWJhamN6aS5naXRodWIuaW8vcHVibGljYXRpb25zL3RhY2FzMjRldGhldGEucGRmfSwKICAgIHVybF9zbGlkZXMgPSB7aHR0cHM6Ly9sZXZlbnRlYmFqY3ppLmdpdGh1Yi5pby9wdWJsaWNhdGlvbnMvc2xpZGVzL3RhY2FzMjRldGhldGEucGRmfSwKICAgIHVybF9tdG10ID0ge2h0dHBzOi8vbTIubXRtdC5odS9hcGkvcHVibGljYXRpb24vMzQ3Njg0MjJ9LAp9Cg==\">\n            <i class=\"fa fa-download fa-fw\"></i> Download BibTeX\n          </a>\n        </li>\n        <li>\n          <a href=\"//bibbase.org/rss?bib=https://leventebajczi.github.io/publications.bib\">\n            <i class=\"fa fa-rss fa-fw\"></i> RSS Feed\n          </a>\n          </li>\n      </ul>\n      </li>\n\n      \n\n\n      \n    </ul>\n\n\n    <div class=\"alert alert-success bibbase_msg\" id=\"bibbase_msg_embed\"\n         style=\"display: none;\">\n\n      Excellent! Next you can\n      <a href=\"/network/register?next=/network/newSiteFromTemplate%3Fbiburl=https://leventebajczi.github.io/publications.bib\"\n      >create a new website with this list</a>, or\n      embed it in an existing web page by copying &amp; pasting\n      any of the following snippets.\n\n      <div style=\"text-align: left; margin-top: 1em;\">\n        <strong>JavaScript</strong>\n        <span class=\"comment recommended\">(easiest)</span>\n        <div class=\"well well-small\">\n          <code>\n            &lt;script src=\"https://bibbase.org/show?bib=https://leventebajczi.github.io%2Fpublications.bib&amp;jsonp=1&amp;theme=side&amp;jsonp=1\"&gt;&lt;/script&gt;\n          </code>\n        </div>\n\n        <strong>PHP</strong>\n        <div class=\"well well-small\">\n          <code>\n            &lt;?php\n            $contents = file_get_contents(\"https://bibbase.org/show?bib=https://leventebajczi.github.io%2Fpublications.bib&amp;jsonp=1&amp;theme=side\");\n            print_r($contents);\n            ?&gt;\n          </code>\n        </div>\n\n        <strong>iFrame</strong>\n        <span class=\"comment\">(not recommended)</span>\n        <div class=\"well well-small\">\n          <code>\n            &lt;iframe src=\"https://bibbase.org/show?bib=https://leventebajczi.github.io%2Fpublications.bib&amp;jsonp=1&amp;theme=side\"&gt;&lt;/iframe&gt;\n          </code>\n        </div>\n\n        <p>\n          For more details see the <a href=\"//bibbase.org/help\">documention</a>.\n        </p>\n      </div>\n    </div>\n\n    <div class=\"alert alert-success bibbase_msg\" id=\"bibbase_msg_preview\"\n         style=\"display: none;\">\n\n      This is a preview! To use this list on your own web site\n      or create a new web site from it,\n      <a href=\"/network/register?next=/network/newAccountWithFile%3FfileId=\"\n      >create a free account</a>. The file will be added\n      and you will be able to edit it in the File Manager.\n      We will show you instructions once you've created your account.\n    </div>\n\n    <div class=\"alert alert-warning bibbase_msg\" id=\"bibbase_msg_mendeley1\"\n         style=\"display: none;\">\n\n      <p>To the site owner:</p>\n\n      <p><strong>Action required!</strong> Mendeley is changing its\n        API. In order to keep using Mendeley with BibBase past April\n        14th, you need to:\n        <ol>\n          <li>renew the authorization for BibBase on Mendeley, and</li>\n          <li>update the BibBase URL\n            in your page the same way you did when you initially set up\n            this page.\n          </li>\n        </ol>\n      </p>\n\n      <p>\n        <a href=\"http://bibbase.org/cgi-bin/mendeley2/get.py\">\n          <i class=\"fa fa-angle-double-right\"></i>\n          Fix it now</a>\n      </p>\n    </div>\n\n  </div>\n\n\n  <div id=\"bibbase_body\">\n    \n  \n  <div class=\"bibbase_group_whole\" id=\"group_2024\">\n    <div class=\"bibbase_group\"\n      onclick=\"toggleGroup('group_2024')\"\n      onkeypress=\"toggleGroup('group_2024')\"\n      tabindex=\"0\">\n      <i class=\"fa fa-angle-down bibbase_group_head_icon\"></i>&nbsp;\n      <span>2024</span>\n      <span class=\"bibbase_group_count\">\n        \n        (3)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\n      \n  \n  <div class=\"bibbase_paper\" id=\"bajczi-dm-micskei-concurrentwitness2testtestharnessingthepowerofconcurrencycompetitioncontribution-2024\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"https://leventebajczi.github.io/publications/tacas24cwt.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'bajczi-dm-micskei-concurrentwitness2testtestharnessingthepowerofconcurrencycompetitioncontribution-2024', 'https://leventebajczi.github.io/publications/tacas24cwt.pdf', event);\">\n    ConcurrentWitness2Test: Test-Harnessing the Power of Concurrency (Competition Contribution).\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"https://leventebajczi.com/publications.html\">Bajczi, L.</a>; Ádám, Z.;  and Micskei, Z. I.\n</span>\n\n  \n\n</span>\n\n  In <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, pages 330-334,  2024. \n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"https://leventebajczi.github.io/publications/tacas24cwt.pdf\"\n     onclick=\"log_download('bajczi-dm-micskei-concurrentwitness2testtestharnessingthepowerofconcurrencycompetitioncontribution-2024', 'https://leventebajczi.github.io/publications/tacas24cwt.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"ConcurrentWitness2Test: Test-Harnessing the Power of Concurrency (Competition Contribution) [pdf]\"\n       title=\" pdf\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\"> pdf</span></a>\n  &nbsp;\n  \n  <a href=\"https://leventebajczi.github.io/publications/slides/tacas24cwt.pdf\"\n     onclick=\"log_download('bajczi-dm-micskei-concurrentwitness2testtestharnessingthepowerofconcurrencycompetitioncontribution-2024', 'https://leventebajczi.github.io/publications/slides/tacas24cwt.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"ConcurrentWitness2Test: Test-Harnessing the Power of Concurrency (Competition Contribution) [pdf]\"\n       title=\" slides\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\"> slides</span></a>\n  &nbsp;\n  \n  <a href=\"https://m2.mtmt.hu/api/publication/34768972\"\n     onclick=\"log_download('bajczi-dm-micskei-concurrentwitness2testtestharnessingthepowerofconcurrencycompetitioncontribution-2024', 'https://m2.mtmt.hu/api/publication/34768972', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"ConcurrentWitness2Test: Test-Harnessing the Power of Concurrency (Competition Contribution) [link]\"\n       title=\" mtmt\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\"> mtmt</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"http://doi.org/10.1007/978-3-031-57256-2_16\"\n     onclick=\"log_download('bajczi-dm-micskei-concurrentwitness2testtestharnessingthepowerofconcurrencycompetitioncontribution-2024', 'http://doi.org/10.1007/978-3-031-57256-2_16', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/bajczi-dm-micskei-concurrentwitness2testtestharnessingthepowerofconcurrencycompetitioncontribution-2024\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n  &nbsp;\n  <span class=\"bibbase_stats_paper\" style=\"color: #777;\">\n    <span>2 downloads</span>\n  </span>\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('bajczi-dm-micskei-concurrentwitness2testtestharnessingthepowerofconcurrencycompetitioncontribution-2024')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@inproceedings{MTMT:34768972,\n\ttitle = {ConcurrentWitness2Test: Test-Harnessing the Power of Concurrency (Competition Contribution)},\n\tauthor = {Bajczi, Levente and Ádám, Zsófia and Micskei, Zoltán Imre},\n\tbooktitle = {Tools and Algorithms for the Construction and Analysis of Systems},\n\tdoi = {10.1007/978-3-031-57256-2_16},\n\tunique-id = {34768972},\n\tabstract = {ConcurrentWitness2Test is a violation witness validator for concurrent software. Taking both nondeterminism of data and interleaving-based nondeterminism into account, the tool aims to use the metadata described in the violation witnesses to synthesize an executable test harness. While plagued by some initial challenges yet to overcome, the validation performance of ConcurrentWitness2Test corroborates the usefulness of the proposed approach.},\n\tyear = {2024},\n\tpages = {330-334},\n\torcid-numbers = {Bajczi, Levente/0000-0002-6551-5860; Ádám, Zsófia/0000-0003-2354-1750; Micskei, Zoltán Imre/0000-0003-1846-261X},\n\n    url_pdf    = {https://leventebajczi.github.io/publications/tacas24cwt.pdf},\n    url_slides = {https://leventebajczi.github.io/publications/slides/tacas24cwt.pdf},\n    url_mtmt = {https://m2.mtmt.hu/api/publication/34768972},\n}\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  ConcurrentWitness2Test is a violation witness validator for concurrent software. Taking both nondeterminism of data and interleaving-based nondeterminism into account, the tool aims to use the metadata described in the violation witnesses to synthesize an executable test harness. While plagued by some initial challenges yet to overcome, the validation performance of ConcurrentWitness2Test corroborates the usefulness of the proposed approach.\n</div>\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"bajczi-telbisz-somorjai-dm-doboskovcs-szekeres-mondok-molnr-thetaabstractionbasedtechniquesforverifyingconcurrencycompetitioncontribution-2024\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"https://leventebajczi.github.io/publications/tacas24theta.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'bajczi-telbisz-somorjai-dm-doboskovcs-szekeres-mondok-molnr-thetaabstractionbasedtechniquesforverifyingconcurrencycompetitioncontribution-2024', 'https://leventebajczi.github.io/publications/tacas24theta.pdf', event);\">\n    Theta: Abstraction Based Techniques for Verifying Concurrency (Competition Contribution).\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"https://leventebajczi.com/publications.html\">Bajczi, L.</a>; Telbisz, C.; Somorjai, M.; Ádám, Z.; Dobos-Kovács, M.; Szekeres, D.; Mondok, M.;  and Molnár, V.\n</span>\n\n  \n\n</span>\n\n  In <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, pages 412-417,  2024. \n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"https://leventebajczi.github.io/publications/tacas24theta.pdf\"\n     onclick=\"log_download('bajczi-telbisz-somorjai-dm-doboskovcs-szekeres-mondok-molnr-thetaabstractionbasedtechniquesforverifyingconcurrencycompetitioncontribution-2024', 'https://leventebajczi.github.io/publications/tacas24theta.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"Theta: Abstraction Based Techniques for Verifying Concurrency (Competition Contribution) [pdf]\"\n       title=\" pdf\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\"> pdf</span></a>\n  &nbsp;\n  \n  <a href=\"https://leventebajczi.github.io/publications/slides/tacas24theta.pdf\"\n     onclick=\"log_download('bajczi-telbisz-somorjai-dm-doboskovcs-szekeres-mondok-molnr-thetaabstractionbasedtechniquesforverifyingconcurrencycompetitioncontribution-2024', 'https://leventebajczi.github.io/publications/slides/tacas24theta.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"Theta: Abstraction Based Techniques for Verifying Concurrency (Competition Contribution) [pdf]\"\n       title=\" slides\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\"> slides</span></a>\n  &nbsp;\n  \n  <a href=\"https://m2.mtmt.hu/api/publication/34768428\"\n     onclick=\"log_download('bajczi-telbisz-somorjai-dm-doboskovcs-szekeres-mondok-molnr-thetaabstractionbasedtechniquesforverifyingconcurrencycompetitioncontribution-2024', 'https://m2.mtmt.hu/api/publication/34768428', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"Theta: Abstraction Based Techniques for Verifying Concurrency (Competition Contribution) [link]\"\n       title=\" mtmt\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\"> mtmt</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"http://doi.org/10.1007/978-3-031-57256-2_30\"\n     onclick=\"log_download('bajczi-telbisz-somorjai-dm-doboskovcs-szekeres-mondok-molnr-thetaabstractionbasedtechniquesforverifyingconcurrencycompetitioncontribution-2024', 'http://doi.org/10.1007/978-3-031-57256-2_30', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/bajczi-telbisz-somorjai-dm-doboskovcs-szekeres-mondok-molnr-thetaabstractionbasedtechniquesforverifyingconcurrencycompetitioncontribution-2024\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n  &nbsp;\n  <span class=\"bibbase_stats_paper\" style=\"color: #777;\">\n    <span>2 downloads</span>\n  </span>\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('bajczi-telbisz-somorjai-dm-doboskovcs-szekeres-mondok-molnr-thetaabstractionbasedtechniquesforverifyingconcurrencycompetitioncontribution-2024')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@inproceedings{MTMT:34768428,\n\ttitle = {Theta: Abstraction Based Techniques for Verifying Concurrency (Competition Contribution)},\n\tauthor = {Bajczi, Levente and Telbisz, Csanád and Somorjai, Márk and Ádám, Zsófia and Dobos-Kovács, Mihály and Szekeres, Dániel and Mondok, Milán and Molnár, Vince},\n\tbooktitle = {Tools and Algorithms for the Construction and Analysis of Systems},\n\tdoi = {10.1007/978-3-031-57256-2_30},\n\tunique-id = {34768428},\n\tabstract = {Theta is a model checking framework, with a strong emphasis on effectively handling concurrency in software using abstraction refinement algorithms. In SV-COMP 2024, we use 1) an abstraction-aware partial order reduction; 2) a dynamic statement reduction technique; and 3) enhanced support for call stacks to handle recursive programs. We integrate these techniques in an improved architecture with inherent support for portfolio-based verification using dynamic algorithm selection, with a diverse selection of supported SMT solvers as well. In this paper we detail the advances of Theta regarding concurrent and recursive software support.},\n\tyear = {2024},\n\tpages = {412-417},\n\torcid-numbers = {Bajczi, Levente/0000-0002-6551-5860; Telbisz, Csanád/0000-0002-6260-5908; Ádám, Zsófia/0000-0003-2354-1750; Dobos-Kovács, Mihály/0000-0002-0064-2965; Szekeres, Dániel/0000-0002-2912-028X; Mondok, Milán/0000-0001-5396-2172; Molnár, Vince/0000-0002-8204-7595},\n\n    url_pdf    = {https://leventebajczi.github.io/publications/tacas24theta.pdf},\n    url_slides = {https://leventebajczi.github.io/publications/slides/tacas24theta.pdf},\n    url_mtmt = {https://m2.mtmt.hu/api/publication/34768428},\n}\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  Theta is a model checking framework, with a strong emphasis on effectively handling concurrency in software using abstraction refinement algorithms. In SV-COMP 2024, we use 1) an abstraction-aware partial order reduction; 2) a dynamic statement reduction technique; and 3) enhanced support for call stacks to handle recursive programs. We integrate these techniques in an improved architecture with inherent support for portfolio-based verification using dynamic algorithm selection, with a diverse selection of supported SMT solvers as well. In this paper we detail the advances of Theta regarding concurrent and recursive software support.\n</div>\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"bajczi-szekeres-mondok-dm-somorjai-telbisz-doboskovcs-molnr-emergenthetaverificationbeyondabstractionrefinementcompetitioncontribution-2024\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"https://leventebajczi.github.io/publications/tacas24etheta.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'bajczi-szekeres-mondok-dm-somorjai-telbisz-doboskovcs-molnr-emergenthetaverificationbeyondabstractionrefinementcompetitioncontribution-2024', 'https://leventebajczi.github.io/publications/tacas24etheta.pdf', event);\">\n    EmergenTheta: Verification Beyond Abstraction Refinement (Competition Contribution).\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"https://leventebajczi.com/publications.html\">Bajczi, L.</a>; Szekeres, D.; Mondok, M.; Ádám, Z.; Somorjai, M.; Telbisz, C.; Dobos-Kovács, M.;  and Molnár, V.\n</span>\n\n  \n\n</span>\n\n  In <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, pages 371-375,  2024. \n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"https://leventebajczi.github.io/publications/tacas24etheta.pdf\"\n     onclick=\"log_download('bajczi-szekeres-mondok-dm-somorjai-telbisz-doboskovcs-molnr-emergenthetaverificationbeyondabstractionrefinementcompetitioncontribution-2024', 'https://leventebajczi.github.io/publications/tacas24etheta.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"EmergenTheta: Verification Beyond Abstraction Refinement (Competition Contribution) [pdf]\"\n       title=\" pdf\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\"> pdf</span></a>\n  &nbsp;\n  \n  <a href=\"https://leventebajczi.github.io/publications/slides/tacas24etheta.pdf\"\n     onclick=\"log_download('bajczi-szekeres-mondok-dm-somorjai-telbisz-doboskovcs-molnr-emergenthetaverificationbeyondabstractionrefinementcompetitioncontribution-2024', 'https://leventebajczi.github.io/publications/slides/tacas24etheta.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"EmergenTheta: Verification Beyond Abstraction Refinement (Competition Contribution) [pdf]\"\n       title=\" slides\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\"> slides</span></a>\n  &nbsp;\n  \n  <a href=\"https://m2.mtmt.hu/api/publication/34768422\"\n     onclick=\"log_download('bajczi-szekeres-mondok-dm-somorjai-telbisz-doboskovcs-molnr-emergenthetaverificationbeyondabstractionrefinementcompetitioncontribution-2024', 'https://m2.mtmt.hu/api/publication/34768422', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"EmergenTheta: Verification Beyond Abstraction Refinement (Competition Contribution) [link]\"\n       title=\" mtmt\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\"> mtmt</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"http://doi.org/10.1007/978-3-031-57256-2_23\"\n     onclick=\"log_download('bajczi-szekeres-mondok-dm-somorjai-telbisz-doboskovcs-molnr-emergenthetaverificationbeyondabstractionrefinementcompetitioncontribution-2024', 'http://doi.org/10.1007/978-3-031-57256-2_23', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/bajczi-szekeres-mondok-dm-somorjai-telbisz-doboskovcs-molnr-emergenthetaverificationbeyondabstractionrefinementcompetitioncontribution-2024\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n  &nbsp;\n  <span class=\"bibbase_stats_paper\" style=\"color: #777;\">\n    <span>1 download</span>\n  </span>\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('bajczi-szekeres-mondok-dm-somorjai-telbisz-doboskovcs-molnr-emergenthetaverificationbeyondabstractionrefinementcompetitioncontribution-2024')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@inproceedings{MTMT:34768422,\n\ttitle = {EmergenTheta: Verification Beyond Abstraction Refinement (Competition Contribution)},\n\tauthor = {Bajczi, Levente and Szekeres, Dániel and Mondok, Milán and Ádám, Zsófia and Somorjai, Márk and Telbisz, Csanád and Dobos-Kovács, Mihály and Molnár, Vince},\n\tbooktitle = {Tools and Algorithms for the Construction and Analysis of Systems},\n\tdoi = {10.1007/978-3-031-57256-2_23},\n\tunique-id = {34768422},\n\tabstract = {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.},\n\tyear = {2024},\n\tpages = {371-375},\n\torcid-numbers = {Bajczi, Levente/0000-0002-6551-5860; Szekeres, Dániel/0000-0002-2912-028X; Mondok, Milán/0000-0001-5396-2172; Ádám, Zsófia/0000-0003-2354-1750; Telbisz, Csanád/0000-0002-6260-5908; Dobos-Kovács, Mihály/0000-0002-0064-2965; Molnár, Vince/0000-0002-8204-7595},\n\n    url_pdf    = {https://leventebajczi.github.io/publications/tacas24etheta.pdf},\n    url_slides = {https://leventebajczi.github.io/publications/slides/tacas24etheta.pdf},\n    url_mtmt = {https://m2.mtmt.hu/api/publication/34768422},\n}\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  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.\n</div>\n\n\n</div>\n\n\n\n\n\n    </div>\n  </div>\n\n  <div class=\"bibbase_group_whole\" id=\"group_2022\">\n    <div class=\"bibbase_group\"\n      onclick=\"toggleGroup('group_2022')\"\n      onkeypress=\"toggleGroup('group_2022')\"\n      tabindex=\"0\">\n      <i class=\"fa fa-angle-down bibbase_group_head_icon\"></i>&nbsp;\n      <span>2022</span>\n      <span class=\"bibbase_group_count\">\n        \n        (2)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\n      \n  \n  <div class=\"bibbase_paper\" id=\"bajczi-dm-molnr-cforyourselfcomparisonoffrontendtechniquesforformalverification-2022\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"https://leventebajczi.github.io/publications/formalise22.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'bajczi-dm-molnr-cforyourselfcomparisonoffrontendtechniquesforformalverification-2022', 'https://leventebajczi.github.io/publications/formalise22.pdf', event);\">\n    C for Yourself: Comparison of Front-End Techniques for Formal Verification.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"https://leventebajczi.com/publications.html\">Bajczi, L.</a>; Ádám, Z.;  and Molnár, V.\n</span>\n\n  \n\n</span>\n\n  In <i>2022 IEEE/ACM 10th International Conference on Formal Methods in Software Engineering (FormaliSE)</i>,  2022. \n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"https://leventebajczi.github.io/publications/formalise22.pdf\"\n     onclick=\"log_download('bajczi-dm-molnr-cforyourselfcomparisonoffrontendtechniquesforformalverification-2022', 'https://leventebajczi.github.io/publications/formalise22.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"C for Yourself: Comparison of Front-End Techniques for Formal Verification [pdf]\"\n       title=\" pdf\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\"> pdf</span></a>\n  &nbsp;\n  \n  <a href=\"https://leventebajczi.github.io/publications/slides/formalise22.pdf\"\n     onclick=\"log_download('bajczi-dm-molnr-cforyourselfcomparisonoffrontendtechniquesforformalverification-2022', 'https://leventebajczi.github.io/publications/slides/formalise22.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"C for Yourself: Comparison of Front-End Techniques for Formal Verification [pdf]\"\n       title=\" slides\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\"> slides</span></a>\n  &nbsp;\n  \n  <a href=\"https://m2.mtmt.hu/api/publication/32836583\"\n     onclick=\"log_download('bajczi-dm-molnr-cforyourselfcomparisonoffrontendtechniquesforformalverification-2022', 'https://m2.mtmt.hu/api/publication/32836583', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"C for Yourself: Comparison of Front-End Techniques for Formal Verification [link]\"\n       title=\" mtmt\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\"> mtmt</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"http://doi.org/10.1145/3524482.3527646\"\n     onclick=\"log_download('bajczi-dm-molnr-cforyourselfcomparisonoffrontendtechniquesforformalverification-2022', 'http://doi.org/10.1145/3524482.3527646', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/bajczi-dm-molnr-cforyourselfcomparisonoffrontendtechniquesforformalverification-2022\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n  &nbsp;\n  <span class=\"bibbase_stats_paper\" style=\"color: #777;\">\n    <span>5 downloads</span>\n  </span>\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('bajczi-dm-molnr-cforyourselfcomparisonoffrontendtechniquesforformalverification-2022')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@inproceedings{MTMT:32836583,\n\ttitle = {C for Yourself: Comparison of Front-End Techniques for Formal Verification},\n\tauthor = {Bajczi, Levente and Ádám, Zsófia and Molnár, Vince},\n\tbooktitle = {2022 IEEE/ACM 10th International Conference on Formal Methods in Software Engineering (FormaliSE)},\n\tdoi = {10.1145/3524482.3527646},\n\tunique-id = {32836583},\n\tyear = {2022},\n\torcid-numbers = {Bajczi, Levente/0000-0002-6551-5860; Ádám, Zsófia/0000-0003-2354-1750; Molnár, Vince/0000-0002-8204-7595},\n\tabstract = {With the improvement of hardware and algorithms, the main challenge of software model checking has shifted from pure algorithmic performance toward supporting a wider set of input programs. Successful toolchains tackle the problem of parsing a wide range of inputs in an efficient way by reusing solutions from existing compiler technologies such as Eclipse CDT or LLVM. Our experience suggests that well-established techniques in compiler technology are not necessarily beneficial to model checkers and sometimes can even hurt their performance. In this paper, we review the tools mature enough to participate in the Software Verification Competition in terms of the employed analysis and frontend techniques. We find that successful tools do exhibit a bias toward certain combinations. We explore the theoretical reasons and suggest an adaptable approach for model checking frameworks. We validate our recommendations by implementing a new frontend for a model checking framework and show that it indeed benefits some of the algorithms.},\n\n    url_pdf    = {https://leventebajczi.github.io/publications/formalise22.pdf},\n    url_slides = {https://leventebajczi.github.io/publications/slides/formalise22.pdf},\n\turl_mtmt = {https://m2.mtmt.hu/api/publication/32836583},\n}\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  With the improvement of hardware and algorithms, the main challenge of software model checking has shifted from pure algorithmic performance toward supporting a wider set of input programs. Successful toolchains tackle the problem of parsing a wide range of inputs in an efficient way by reusing solutions from existing compiler technologies such as Eclipse CDT or LLVM. Our experience suggests that well-established techniques in compiler technology are not necessarily beneficial to model checkers and sometimes can even hurt their performance. In this paper, we review the tools mature enough to participate in the Software Verification Competition in terms of the employed analysis and frontend techniques. We find that successful tools do exhibit a bias toward certain combinations. We explore the theoretical reasons and suggest an adaptable approach for model checking frameworks. We validate our recommendations by implementing a new frontend for a model checking framework and show that it indeed benefits some of the algorithms.\n</div>\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"dm-bajczi-doboskovcs-hajdu-molnr-thetaportfolioofcegarbasedanalyseswithdynamicalgorithmselectioncompetitioncontribution-2022\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"https://leventebajczi.github.io/publications/tacas22.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'dm-bajczi-doboskovcs-hajdu-molnr-thetaportfolioofcegarbasedanalyseswithdynamicalgorithmselectioncompetitioncontribution-2022', 'https://leventebajczi.github.io/publications/tacas22.pdf', event);\">\n    Theta: portfolio of CEGAR-based analyses with dynamic algorithm selection (Competition Contribution).\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  Ádám, Z.; <a class=\"bibbase author link\" href=\"https://leventebajczi.com/publications.html\">Bajczi, L.</a>; Dobos-Kovács, M.; Hajdu, Á.;  and Molnár, V.\n</span>\n\n  \n\n</span>\n\n  <i>LECTURE NOTES IN COMPUTER SCIENCE</i>, 13244: 474-478.  2022.\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"https://leventebajczi.github.io/publications/tacas22.pdf\"\n     onclick=\"log_download('dm-bajczi-doboskovcs-hajdu-molnr-thetaportfolioofcegarbasedanalyseswithdynamicalgorithmselectioncompetitioncontribution-2022', 'https://leventebajczi.github.io/publications/tacas22.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"Theta: portfolio of CEGAR-based analyses with dynamic algorithm selection (Competition Contribution) [pdf]\"\n       title=\" pdf\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\"> pdf</span></a>\n  &nbsp;\n  \n  <a href=\"https://leventebajczi.github.io/publications/slides/tacas22.pdf\"\n     onclick=\"log_download('dm-bajczi-doboskovcs-hajdu-molnr-thetaportfolioofcegarbasedanalyseswithdynamicalgorithmselectioncompetitioncontribution-2022', 'https://leventebajczi.github.io/publications/slides/tacas22.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"Theta: portfolio of CEGAR-based analyses with dynamic algorithm selection (Competition Contribution) [pdf]\"\n       title=\" slides\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\"> slides</span></a>\n  &nbsp;\n  \n  <a href=\"https://leventebajczi.github.io/publications/posters/tacas22.pdf\"\n     onclick=\"log_download('dm-bajczi-doboskovcs-hajdu-molnr-thetaportfolioofcegarbasedanalyseswithdynamicalgorithmselectioncompetitioncontribution-2022', 'https://leventebajczi.github.io/publications/posters/tacas22.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"Theta: portfolio of CEGAR-based analyses with dynamic algorithm selection (Competition Contribution) [pdf]\"\n       title=\" poster\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\"> poster</span></a>\n  &nbsp;\n  \n  <a href=\"https://m2.mtmt.hu/api/publication/32801008\"\n     onclick=\"log_download('dm-bajczi-doboskovcs-hajdu-molnr-thetaportfolioofcegarbasedanalyseswithdynamicalgorithmselectioncompetitioncontribution-2022', 'https://m2.mtmt.hu/api/publication/32801008', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"Theta: portfolio of CEGAR-based analyses with dynamic algorithm selection (Competition Contribution) [link]\"\n       title=\" mtmt\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\"> mtmt</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"http://doi.org/10.1007/978-3-030-99527-0_34\"\n     onclick=\"log_download('dm-bajczi-doboskovcs-hajdu-molnr-thetaportfolioofcegarbasedanalyseswithdynamicalgorithmselectioncompetitioncontribution-2022', 'http://doi.org/10.1007/978-3-030-99527-0_34', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/dm-bajczi-doboskovcs-hajdu-molnr-thetaportfolioofcegarbasedanalyseswithdynamicalgorithmselectioncompetitioncontribution-2022\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n  &nbsp;\n  <span class=\"bibbase_stats_paper\" style=\"color: #777;\">\n    <span>8 downloads</span>\n  </span>\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('dm-bajczi-doboskovcs-hajdu-molnr-thetaportfolioofcegarbasedanalyseswithdynamicalgorithmselectioncompetitioncontribution-2022')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n  \n  \n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@article{MTMT:32801008,\n\ttitle = {Theta: portfolio of CEGAR-based analyses with dynamic algorithm selection (Competition Contribution)},\n\tauthor = {Ádám, Zsófia and Bajczi, Levente and Dobos-Kovács, Mihály and Hajdu, Ákos and Molnár, Vince},\n\tdoi = {10.1007/978-3-030-99527-0_34},\n\tjournal-iso = {LECT NOTES COMPUT SC},\n\tjournal = {LECTURE NOTES IN COMPUTER SCIENCE},\n\tvolume = {13244},\n\tunique-id = {32801008},\n\tissn = {0302-9743},\n\tkeywords = {Computer Science, Software Engineering},\n\tyear = {2022},\n\teissn = {1611-3349},\n\tpages = {474-478},\n\torcid-numbers = {Ádám, Zsófia/0000-0003-2354-1750; Bajczi, Levente/0000-0002-6551-5860; Dobos-Kovács, Mihály/0000-0002-0064-2965; Hajdu, Ákos/0000-0001-8001-8865; Molnár, Vince/0000-0002-8204-7595},\n\tabstract = {THETA is a model checking framework based on abstraction refinement algorithms. In SV-COMP 2022, we introduce: 1) reasoning at the source-level via a direct translation from C programs; 2) support for concurrent programs with interleaving semantics; 3) mitigation for non-progressing refinement loops; 4) support for SMT-LIB-compliant solvers. We combine all of the aforementioned techniques into a portfolio with dynamic algorithm selection.},\n\n    url_pdf    = {https://leventebajczi.github.io/publications/tacas22.pdf},\n    url_slides = {https://leventebajczi.github.io/publications/slides/tacas22.pdf},\n    url_poster = {https://leventebajczi.github.io/publications/posters/tacas22.pdf},\n\turl_mtmt = {https://m2.mtmt.hu/api/publication/32801008},\n}\n\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  THETA is a model checking framework based on abstraction refinement algorithms. In SV-COMP 2022, we introduce: 1) reasoning at the source-level via a direct translation from C programs; 2) support for concurrent programs with interleaving semantics; 3) mitigation for non-progressing refinement loops; 4) support for SMT-LIB-compliant solvers. We combine all of the aforementioned techniques into a portfolio with dynamic algorithm selection.\n</div>\n\n\n</div>\n\n\n\n\n\n    </div>\n  </div>\n\n  <div class=\"bibbase_group_whole\" id=\"group_2019\">\n    <div class=\"bibbase_group\"\n      onclick=\"toggleGroup('group_2019')\"\n      onkeypress=\"toggleGroup('group_2019')\"\n      tabindex=\"0\">\n      <i class=\"fa fa-angle-down bibbase_group_head_icon\"></i>&nbsp;\n      <span>2019</span>\n      <span class=\"bibbase_group_count\">\n        \n        (1)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\n      \n  \n  <div class=\"bibbase_paper\" id=\"bajczi-vrs-molnr-willmyprogrambreakonthisfaultyprocessorformalanalysisofhardwarefaultactivationsinconcurrentembeddedsoftware-2019\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"https://leventebajczi.github.io/publications/emsoft19.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'bajczi-vrs-molnr-willmyprogrambreakonthisfaultyprocessorformalanalysisofhardwarefaultactivationsinconcurrentembeddedsoftware-2019', 'https://leventebajczi.github.io/publications/emsoft19.pdf', event);\">\n    Will My Program Break on This Faulty Processor?. Formal Analysis of Hardware Fault Activations in Concurrent Embedded Software.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"https://leventebajczi.com/publications.html\">Bajczi, L.</a>; Vörös, A.;  and Molnár, V.\n</span>\n\n  \n\n</span>\n\n  <i>ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS</i>, 18.  2019.\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"https://leventebajczi.github.io/publications/emsoft19.pdf\"\n     onclick=\"log_download('bajczi-vrs-molnr-willmyprogrambreakonthisfaultyprocessorformalanalysisofhardwarefaultactivationsinconcurrentembeddedsoftware-2019', 'https://leventebajczi.github.io/publications/emsoft19.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"Will My Program Break on This Faulty Processor?. Formal Analysis of Hardware Fault Activations in Concurrent Embedded Software [pdf]\"\n       title=\" pdf\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\"> pdf</span></a>\n  &nbsp;\n  \n  <a href=\"https://leventebajczi.github.io/publications/slides/emsoft19.pdf\"\n     onclick=\"log_download('bajczi-vrs-molnr-willmyprogrambreakonthisfaultyprocessorformalanalysisofhardwarefaultactivationsinconcurrentembeddedsoftware-2019', 'https://leventebajczi.github.io/publications/slides/emsoft19.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"Will My Program Break on This Faulty Processor?. Formal Analysis of Hardware Fault Activations in Concurrent Embedded Software [pdf]\"\n       title=\" slides\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\"> slides</span></a>\n  &nbsp;\n  \n  <a href=\"https://m2.mtmt.hu/api/publication/30865515\"\n     onclick=\"log_download('bajczi-vrs-molnr-willmyprogrambreakonthisfaultyprocessorformalanalysisofhardwarefaultactivationsinconcurrentembeddedsoftware-2019', 'https://m2.mtmt.hu/api/publication/30865515', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"Will My Program Break on This Faulty Processor?. Formal Analysis of Hardware Fault Activations in Concurrent Embedded Software [link]\"\n       title=\" mtmt\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\"> mtmt</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"http://doi.org/10.1145/3358238\"\n     onclick=\"log_download('bajczi-vrs-molnr-willmyprogrambreakonthisfaultyprocessorformalanalysisofhardwarefaultactivationsinconcurrentembeddedsoftware-2019', 'http://doi.org/10.1145/3358238', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/bajczi-vrs-molnr-willmyprogrambreakonthisfaultyprocessorformalanalysisofhardwarefaultactivationsinconcurrentembeddedsoftware-2019\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('bajczi-vrs-molnr-willmyprogrambreakonthisfaultyprocessorformalanalysisofhardwarefaultactivationsinconcurrentembeddedsoftware-2019')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@article{MTMT:30865515,\n\ttitle = {Will My Program Break on This Faulty Processor?. Formal Analysis of Hardware Fault Activations in Concurrent Embedded Software},\n\tauthor = {Bajczi, Levente and Vörös, András and Molnár, Vince},\n\tdoi = {10.1145/3358238},\n\tjournal-iso = {ACM T EMBED COMPUT S},\n\tjournal = {ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS},\n\tvolume = {18},\n\tunique-id = {30865515},\n\tissn = {1539-9087},\n\tabstract = {Formal verification is approaching a point where it will be reliably applicable to embedded software. Even though formal verification can efficiently analyze multi-threaded applications, multi-core processors are often considered too dangerous to use in critical systems, despite the many benefits they can offer. One reason is the advanced memory consistency model of such CPUs. Nowadays, most software verifiers assume strict sequential consistency, which is also the naïve view of programmers. Modern multi-core processors, however, rarely guarantee this assumption by default. In addition, complex processor architectures may easily contain design faults. Thanks to the recent advances in hardware verification, these faults are increasingly visible and can be detected even in existing processors, giving an opportunity to compensate for the problem in software. In this paper, we propose a generic approach to consider inconsistent behavior of the hardware in the analysis of software. Our approach is based on formal methods and can be used to detect the activation of existing hardware faults on the application level and facilitate their mitigation in software. The approach relies heavily on recent results of model checking and hardware verification and offers new, integrative research directions. We propose a partial solution based on existing model checking tools to demonstrate feasibility and evaluate their performance in this context.},\n\tyear = {2019},\n\teissn = {1558-3465},\n\torcid-numbers = {Bajczi, Levente/0000-0002-6551-5860; Molnár, Vince/0000-0002-8204-7595},\n\n    url_pdf    = {https://leventebajczi.github.io/publications/emsoft19.pdf},\n    url_slides = {https://leventebajczi.github.io/publications/slides/emsoft19.pdf},\n\turl_mtmt = {https://m2.mtmt.hu/api/publication/30865515},\t\n}\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  Formal verification is approaching a point where it will be reliably applicable to embedded software. Even though formal verification can efficiently analyze multi-threaded applications, multi-core processors are often considered too dangerous to use in critical systems, despite the many benefits they can offer. One reason is the advanced memory consistency model of such CPUs. Nowadays, most software verifiers assume strict sequential consistency, which is also the naïve view of programmers. Modern multi-core processors, however, rarely guarantee this assumption by default. In addition, complex processor architectures may easily contain design faults. Thanks to the recent advances in hardware verification, these faults are increasingly visible and can be detected even in existing processors, giving an opportunity to compensate for the problem in software. In this paper, we propose a generic approach to consider inconsistent behavior of the hardware in the analysis of software. Our approach is based on formal methods and can be used to detect the activation of existing hardware faults on the application level and facilitate their mitigation in software. The approach relies heavily on recent results of model checking and hardware verification and offers new, integrative research directions. We propose a partial solution based on existing model checking tools to demonstrate feasibility and evaluate their performance in this context.\n</div>\n\n\n</div>\n\n\n\n\n\n    </div>\n  </div>\n\n\n\n\n  </div>\n\n\n  <!-- Modal -->\n\n  <!-- <iframe id=\"bibbase_network_frame\" -->\n  <!--         src=\"//bibbase.org/network/control\" -->\n  <!--         style=\"display: none;\"> -->\n  <!-- </iframe> -->\n\n</div>\n"}; document.write(bibbase_data.data);