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\",\"ssl\":false},\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\":6,\"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\"}},\"downloads\":1,\"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\":4,\"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\":5,\"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\\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\":2,\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"inproceedings\",\"title\":\"Verbesserung der MBSE-Ausbildung durch Versionskontrolle und automatisiertes Feedback\",\"author\":[{\"propositions\":[],\"lastnames\":[\"Bajczi\"],\"firstnames\":[\"Levente\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Szekeres\"],\"firstnames\":[\"Dániel\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Siegl\"],\"firstnames\":[\"Daniel\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Molnár\"],\"firstnames\":[\"Vince\"],\"suffixes\":[]}],\"booktitle\":\"Tag des Systems Engineering\",\"unique-id\":\"35617761\",\"year\":\"2024\",\"pages\":\"161-169\",\"orcid-numbers\":\"Bajczi, Levente/0000-0002-6551-5860; Szekeres, Dániel/0000-0002-2912-028X; Molnár, Vince/0000-0002-8204-7595\",\"url_pdf\":\"https://leventebajczi.github.io/publications/tdse24verbesserung.pdf\",\"url_slides\":\"https://leventebajczi.github.io/publications/slides/tdse24verbesserung.pdf\",\"url_mtmt\":\"https://m2.mtmt.hu/api/publication/35617761\",\"bibtex\":\"@inproceedings{MTMT:35617761,\\n\\ttitle = {Verbesserung der MBSE-Ausbildung durch Versionskontrolle und automatisiertes Feedback},\\n\\tauthor = {Bajczi, Levente and Szekeres, Dániel and Siegl, Daniel and Molnár, Vince},\\n\\tbooktitle = {Tag des Systems Engineering},\\n\\tunique-id = {35617761},\\n\\tyear = {2024},\\n\\tpages = {161-169},\\n\\torcid-numbers = {Bajczi, Levente/0000-0002-6551-5860; Szekeres, Dániel/0000-0002-2912-028X; Molnár, Vince/0000-0002-8204-7595},\\n\\n    url_pdf    = {https://leventebajczi.github.io/publications/tdse24verbesserung.pdf},\\n    url_slides = {https://leventebajczi.github.io/publications/slides/tdse24verbesserung.pdf},\\n    url_mtmt = {https://m2.mtmt.hu/api/publication/35617761},\\n}\\n\\n\",\"author_short\":[\"Bajczi, L.\",\"Szekeres, D.\",\"Siegl, D.\",\"Molnár, V.\"],\"key\":\"MTMT:35617761\",\"id\":\"MTMT:35617761\",\"bibbaseid\":\"bajczi-szekeres-siegl-molnr-verbesserungdermbseausbildungdurchversionskontrolleundautomatisiertesfeedback-2024\",\"role\":\"author\",\"urls\":{\" pdf\":\"https://leventebajczi.github.io/publications/tdse24verbesserung.pdf\",\" slides\":\"https://leventebajczi.github.io/publications/slides/tdse24verbesserung.pdf\",\" mtmt\":\"https://m2.mtmt.hu/api/publication/35617761\"},\"metadata\":{\"authorlinks\":{\"bajczi, l\":\"https://leventebajczi.com/publications.html\"}},\"downloads\":1,\"html\":\"\"},{\"bibtype\":\"misc\",\"type\":\"misc\",\"title\":\"Enhancing MBSE Education with Version Control and Automated Feedback\",\"author\":[{\"firstnames\":[\"Levente\"],\"propositions\":[],\"lastnames\":[\"Bajczi\"],\"suffixes\":[]},{\"firstnames\":[\"Dániel\"],\"propositions\":[],\"lastnames\":[\"Szekeres\"],\"suffixes\":[]},{\"firstnames\":[\"Daniel\"],\"propositions\":[],\"lastnames\":[\"Siegl\"],\"suffixes\":[]},{\"firstnames\":[\"Vince\"],\"propositions\":[],\"lastnames\":[\"Molnár\"],\"suffixes\":[]}],\"year\":\"2024\",\"eprint\":\"2409.15294\",\"archiveprefix\":\"arXiv\",\"primaryclass\":\"cs.CY\",\"url_pdf\":\"https://leventebajczi.github.io/publications/tdse24enhancing.pdf\",\"url_slides\":\"https://leventebajczi.github.io/publications/slides/tdse24verbesserung.pdf\",\"bibtex\":\"@misc{bajczi2024enhancingmbseeducationversion,\\n\\ttitle={Enhancing MBSE Education with Version Control and Automated Feedback}, \\n\\tauthor={Levente Bajczi and Dániel Szekeres and Daniel Siegl and Vince Molnár},\\n\\tyear={2024},\\n\\teprint={2409.15294},\\n\\tarchivePrefix={arXiv},\\n\\tprimaryClass={cs.CY},\\n\\n\\turl_pdf    = {https://leventebajczi.github.io/publications/tdse24enhancing.pdf},\\n    url_slides = {https://leventebajczi.github.io/publications/slides/tdse24verbesserung.pdf},\\n}\\n\\n\\n\",\"author_short\":[\"Bajczi, L.\",\"Szekeres, D.\",\"Siegl, D.\",\"Molnár, V.\"],\"key\":\"bajczi2024enhancingmbseeducationversion\",\"id\":\"bajczi2024enhancingmbseeducationversion\",\"bibbaseid\":\"bajczi-szekeres-siegl-molnr-enhancingmbseeducationwithversioncontrolandautomatedfeedback-2024\",\"role\":\"author\",\"urls\":{\" pdf\":\"https://leventebajczi.github.io/publications/tdse24enhancing.pdf\",\" slides\":\"https://leventebajczi.github.io/publications/slides/tdse24verbesserung.pdf\"},\"metadata\":{\"authorlinks\":{\"bajczi, l\":\"https://leventebajczi.com/publications.html\"}},\"html\":\"\"},{\"bibtype\":\"article\",\"type\":\"article\",\"title\":\"NetworCat: applying analysis techniques of shared memory software on message-passing distributed systems\",\"author\":[{\"propositions\":[],\"lastnames\":[\"Bajczi\"],\"firstnames\":[\"Levente\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Molnár\"],\"firstnames\":[\"Vince\"],\"suffixes\":[]}],\"doi\":\"10.1007/s10270-024-01258-x\",\"journal-iso\":\"SOFTW SYST MODEL\",\"journal\":\"SOFTWARE AND SYSTEMS MODELING\",\"unique-id\":\"35762171\",\"issn\":\"1619-1366\",\"abstract\":\"Communication models are a key aspect in the design and implementation of distributed system architectures. Application logic must consider the guarantees of these models, which fundamentally influence its correctness. Modern multi-core processor architectures face a similar problem when it comes to accessing shared memory: the guarantees of an architecture have a fundamental impact on the observable behavior of software. The formalization of these guarantees in a declarative way has led to powerful tools and algorithms to define reusable constraints on patterns of memory access events and their relationships, enabling the efficient description and automatic formal analysis of software properties with respect to a specific architecture. The Cat memory modeling language provides a standard means of specifying these constraints. Despite the parallels, the axiomatic modeling and analysis of communication models in distributed systems remain a relatively unexplored area. In this paper, we address this gap and demonstrate how communication models can be mapped to the Cat language. We create a standard library of reusable patterns and demonstrate our approach, called NetworCat , on the simple examples of UDP and TCP, and we also present its applicability to the vastly configurable OMG-DDS service. This adaptation-based approach enables the use of ever-improving verification tools built for shared memory concurrency on distributed systems. We believe this not only benefits distributed system analyses by broadening the toolset for verification but also positively impacts the field of memory-model-aware verification by widening its audience to another domain.\",\"year\":\"2025\",\"eissn\":\"1619-1374\",\"orcid-numbers\":\"Bajczi, Levente/0000-0002-6551-5860; Molnár, Vince/0000-0002-8204-7595\",\"url_pdf\":\"https://leventebajczi.github.io/publications/sosym25networcat.pdf\",\"url_mtmt\":\"https://m2.mtmt.hu/api/publication/35762171\",\"bibtex\":\"@article{MTMT:35762171,\\n\\ttitle = {{NetworCat: applying analysis techniques of shared memory software on message-passing distributed systems}},\\n\\tauthor = {Bajczi, Levente and Molnár, Vince},\\n\\tdoi = {10.1007/s10270-024-01258-x},\\n\\tjournal-iso = {SOFTW SYST MODEL},\\n\\tjournal = {SOFTWARE AND SYSTEMS MODELING},\\n\\tunique-id = {35762171},\\n\\tissn = {1619-1366},\\n\\tabstract = {Communication models are a key aspect in the design and implementation of distributed system architectures. Application logic must consider the guarantees of these models, which fundamentally influence its correctness. Modern multi-core processor architectures face a similar problem when it comes to accessing shared memory: the guarantees of an architecture have a fundamental impact on the observable behavior of software. The formalization of these guarantees in a declarative way has led to powerful tools and algorithms to define reusable constraints on patterns of memory access events and their relationships, enabling the efficient description and automatic formal analysis of software properties with respect to a specific architecture. The Cat memory modeling language provides a standard means of specifying these constraints. Despite the parallels, the axiomatic modeling and analysis of communication models in distributed systems remain a relatively unexplored area. In this paper, we address this gap and demonstrate how communication models can be mapped to the Cat language. We create a standard library of reusable patterns and demonstrate our approach, called NetworCat , on the simple examples of UDP and TCP, and we also present its applicability to the vastly configurable OMG-DDS service. This adaptation-based approach enables the use of ever-improving verification tools built for shared memory concurrency on distributed systems. We believe this not only benefits distributed system analyses by broadening the toolset for verification but also positively impacts the field of memory-model-aware verification by widening its audience to another domain.},\\n\\tyear = {2025},\\n\\teissn = {1619-1374},\\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/sosym25networcat.pdf},\\n\\turl_mtmt   = {https://m2.mtmt.hu/api/publication/35762171},\\n}\\n\\n\",\"author_short\":[\"Bajczi, L.\",\"Molnár, V.\"],\"key\":\"MTMT:35762171\",\"id\":\"MTMT:35762171\",\"bibbaseid\":\"bajczi-molnr-networcatapplyinganalysistechniquesofsharedmemorysoftwareonmessagepassingdistributedsystems-2025\",\"role\":\"author\",\"urls\":{\" pdf\":\"https://leventebajczi.github.io/publications/sosym25networcat.pdf\",\" mtmt\":\"https://m2.mtmt.hu/api/publication/35762171\"},\"metadata\":{\"authorlinks\":{\"bajczi, l\":\"https://leventebajczi.com/publications.html\"}},\"html\":\"\"},{\"bibtype\":\"article\",\"type\":\"article\",\"title\":\"Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification\",\"author\":[{\"propositions\":[],\"lastnames\":[\"Somorjai\"],\"firstnames\":[\"Márk\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Dobos-Kovács\"],\"firstnames\":[\"Mihály\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Ádám\"],\"firstnames\":[\"Zsófia\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Bajczi\"],\"firstnames\":[\"Levente\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Vörös\"],\"firstnames\":[\"András\"],\"suffixes\":[]}],\"doi\":\"10.4204/EPTCS.402.11\",\"journal-iso\":\"ELECTRON PROC THEOR COMPUT SCI\",\"journal\":\"ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE\",\"volume\":\"402\",\"unique-id\":\"33784283\",\"abstract\":\"Constrained Horn Clauses (CHCs) have conventionally been used as a low-level representation in formal verification. Most existing solvers use a diverse set of specialized techniques, including direct state space traversal or under-approximating abstraction, necessitating purpose-built complex algorithms. Other solvers successfully simplified the verification workflow by translating the problem to inputs for other verification tasks, leveraging the strengths of existing algorithms. One such approach transforms the CHC problem into a recursive program roughly emulating a top-down solver for the deduction task; and verifying the reachability of a safety violation specified as a control location. We propose an alternative bottom-up approach for linear CHCs, and evaluate the two options in the open-source model checking framework THETA on both synthetic and industrial examples. We find that there is a more than twofold increase in the number of solved tasks when the novel bottom-up approach is used in the verification workflow, in contrast with the top-down technique. © Márk Somorjai et al.\",\"year\":\"2024\",\"eissn\":\"2075-2180\",\"pages\":\"105-117\",\"orcid-numbers\":\"Dobos-Kovács, Mihály/0000-0002-0064-2965; Ádám, Zsófia/0000-0003-2354-1750; Bajczi, Levente/0000-0002-6551-5860\",\"url_pdf\":\"https://leventebajczi.github.io/publications/hcvs24chc.pdf\",\"url_mtmt\":\"https://m2.mtmt.hu/api/publication/33784283\",\"bibtex\":\"@article{MTMT:33784283,\\n\\ttitle = {Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification},\\n\\tauthor = {Somorjai, Márk and Dobos-Kovács, Mihály and Ádám, Zsófia and Bajczi, Levente and Vörös, András},\\n\\tdoi = {10.4204/EPTCS.402.11},\\n\\tjournal-iso = {ELECTRON PROC THEOR COMPUT SCI},\\n\\tjournal = {ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE},\\n\\tvolume = {402},\\n\\tunique-id = {33784283},\\n\\tabstract = {Constrained Horn Clauses (CHCs) have conventionally been used as a low-level representation in formal verification. Most existing solvers use a diverse set of specialized techniques, including direct state space traversal or under-approximating abstraction, necessitating purpose-built complex algorithms. Other solvers successfully simplified the verification workflow by translating the problem to inputs for other verification tasks, leveraging the strengths of existing algorithms. One such approach transforms the CHC problem into a recursive program roughly emulating a top-down solver for the deduction task; and verifying the reachability of a safety violation specified as a control location. We propose an alternative bottom-up approach for linear CHCs, and evaluate the two options in the open-source model checking framework THETA on both synthetic and industrial examples. We find that there is a more than twofold increase in the number of solved tasks when the novel bottom-up approach is used in the verification workflow, in contrast with the top-down technique. © Márk Somorjai et al.},\\n\\tyear = {2024},\\n\\teissn = {2075-2180},\\n\\tpages = {105-117},\\n\\torcid-numbers = {Dobos-Kovács, Mihály/0000-0002-0064-2965; Ádám, Zsófia/0000-0003-2354-1750; Bajczi, Levente/0000-0002-6551-5860},\\n\\n    url_pdf    = {https://leventebajczi.github.io/publications/hcvs24chc.pdf},\\n\\turl_mtmt   = {https://m2.mtmt.hu/api/publication/33784283},\\t\\n}\\n\\n\",\"author_short\":[\"Somorjai, M.\",\"Dobos-Kovács, M.\",\"Ádám, Z.\",\"Bajczi, L.\",\"Vörös, A.\"],\"key\":\"MTMT:33784283\",\"id\":\"MTMT:33784283\",\"bibbaseid\":\"somorjai-doboskovcs-dm-bajczi-vrs-bottomsupforchcsnoveltransformationoflinearconstrainedhornclausestosoftwareverification-2024\",\"role\":\"author\",\"urls\":{\" pdf\":\"https://leventebajczi.github.io/publications/hcvs24chc.pdf\",\" mtmt\":\"https://m2.mtmt.hu/api/publication/33784283\"},\"metadata\":{\"authorlinks\":{\"bajczi, l\":\"https://leventebajczi.com/publications.html\"}},\"html\":\"\"},{\"bibtype\":\"article\",\"type\":\"article\",\"title\":\"Solving Constrained Horn Clauses as C Programs with CHC2C\",\"author\":[{\"propositions\":[],\"lastnames\":[\"Bajczi\"],\"firstnames\":[\"Levente\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Molnár\"],\"firstnames\":[\"Vince\"],\"suffixes\":[]}],\"doi\":\"10.1007/978-3-031-66149-5_8\",\"journal-iso\":\"LNCS\",\"journal\":\"LECTURE NOTES IN COMPUTER SCIENCE\",\"volume\":\"14624\",\"unique-id\":\"34853031\",\"issn\":\"0302-9743\",\"abstract\":\"Solving Constrained Horn Clauses (CHC) is necessitated by numerous fields in formal methods, from verifying software and smart contracts to modeling systems, yet the competitive scene for academic tools remains fairly sparse, especially compared to more popular fields such as software verification. Comparative evaluation as a competition, such as SV-COMP or CHC-COMP, sparks a more cohesive community around fields in formal methods. Lately, a trend has been emerging with tools such as Btor2C that bridge multiple fields together, thus widening this cohesion. Following that example, we propose and perform an experiment, where we use CHC-to-C transformation to apply software verification tools to linear CHC problems. In the process, we help both fields by diversifying the scene of CHC solvers and providing new and valuable benchmarks to aid the development of software verification tools. Using these benchmarks, we uncovered a previously hidden bug in multiple verification tools that can lead to false positive results. By analysing the results of the experiment, we can confidently make a recommendation for developers of software verifiers to consider supporting CHCs via our pre-verification transformation.\",\"keywords\":\"verification; formal methods; Computer Science, Software Engineering; CHC\",\"year\":\"2024\",\"eissn\":\"1611-3349\",\"pages\":\"146-163\",\"orcid-numbers\":\"Bajczi, Levente/0000-0002-6551-5860; Molnár, Vince/0000-0002-8204-7595\",\"url_pdf\":\"https://leventebajczi.github.io/publications/spin24chc2c.pdf\",\"url_slides\":\"https://leventebajczi.github.io/publications/slides/spin24chc2c.pdf\",\"url_mtmt\":\"https://m2.mtmt.hu/api/publication/34853031\",\"bibtex\":\"@article{MTMT:34853031,\\n\\ttitle = {Solving Constrained Horn Clauses as C Programs with CHC2C},\\n\\tauthor = {Bajczi, Levente and Molnár, Vince},\\n\\tdoi = {10.1007/978-3-031-66149-5_8},\\n\\tjournal-iso = {LNCS},\\n\\tjournal = {LECTURE NOTES IN COMPUTER SCIENCE},\\n\\tvolume = {14624},\\n\\tunique-id = {34853031},\\n\\tissn = {0302-9743},\\n\\tabstract = {Solving Constrained Horn Clauses (CHC) is necessitated by numerous fields in formal methods, from verifying software and smart contracts to modeling systems, yet the competitive scene for academic tools remains fairly sparse, especially compared to more popular fields such as software verification. Comparative evaluation as a competition, such as SV-COMP or CHC-COMP, sparks a more cohesive community around fields in formal methods. Lately, a trend has been emerging with tools such as Btor2C that bridge multiple fields together, thus widening this cohesion. Following that example, we propose and perform an experiment, where we use CHC-to-C transformation to apply software verification tools to linear CHC problems. In the process, we help both fields by diversifying the scene of CHC solvers and providing new and valuable benchmarks to aid the development of software verification tools. Using these benchmarks, we uncovered a previously hidden bug in multiple verification tools that can lead to false positive results. By analysing the results of the experiment, we can confidently make a recommendation for developers of software verifiers to consider supporting CHCs via our pre-verification transformation.},\\n\\tkeywords = {verification; formal methods; Computer Science, Software Engineering; CHC},\\n\\tyear = {2024},\\n\\teissn = {1611-3349},\\n\\tpages = {146-163},\\n\\torcid-numbers = {Bajczi, Levente/0000-0002-6551-5860; Molnár, Vince/0000-0002-8204-7595},\\n\\n\\n    url_pdf    = {https://leventebajczi.github.io/publications/spin24chc2c.pdf},\\n    url_slides = {https://leventebajczi.github.io/publications/slides/spin24chc2c.pdf},\\n\\turl_mtmt   = {https://m2.mtmt.hu/api/publication/34853031},\\t\\n}\\n\\n\",\"author_short\":[\"Bajczi, L.\",\"Molnár, V.\"],\"key\":\"MTMT:34853031\",\"id\":\"MTMT:34853031\",\"bibbaseid\":\"bajczi-molnr-solvingconstrainedhornclausesascprogramswithchc2c-2024\",\"role\":\"author\",\"urls\":{\" pdf\":\"https://leventebajczi.github.io/publications/spin24chc2c.pdf\",\" slides\":\"https://leventebajczi.github.io/publications/slides/spin24chc2c.pdf\",\" mtmt\":\"https://m2.mtmt.hu/api/publication/34853031\"},\"keyword\":[\"verification; formal methods; Computer Science\",\"Software Engineering; CHC\"],\"metadata\":{\"authorlinks\":{\"bajczi, l\":\"https://leventebajczi.com/publications.html\"}},\"html\":\"\"},{\"bibtype\":\"article\",\"type\":\"article\",\"title\":\"Theta: Various Approaches for Concurrent Program Verification (Competition Contribution)\",\"author\":[{\"propositions\":[],\"lastnames\":[\"Telbisz\"],\"firstnames\":[\"Csanád\",\"Ferenc\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Bajczi\"],\"firstnames\":[\"Levente\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Szekeres\"],\"firstnames\":[\"Dániel\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Vörös\"],\"firstnames\":[\"András\"],\"suffixes\":[]}],\"doi\":\"10.1007/978-3-031-90660-2_22\",\"journal-iso\":\"LNCS\",\"journal\":\"LECTURE NOTES IN COMPUTER SCIENCE\",\"volume\":\"15698\",\"unique-id\":\"36122885\",\"issn\":\"0302-9743\",\"abstract\":\"Theta is a model checking framework with a strong emphasis on effectively handling concurrency in software using abstraction refinement algorithms. In SV-COMP 2025, we complement our existing approach (abstraction-aware partial order reduction) for multi-threaded programs with a happens before propagator-based BMC check, expecting a significant increase in performance. We again utilize our portfolio with dynamic algorithm selection from last year, with improvements regarding solver choice and configuration ordering. In this paper, we detail our algorithmic improvements in Theta regarding the verification of concurrent software.\",\"year\":\"2025\",\"eissn\":\"1611-3349\",\"pages\":\"260-265\",\"orcid-numbers\":\"Telbisz, Csanád Ferenc/0000-0002-6260-5908; Bajczi, Levente/0000-0002-6551-5860; Szekeres, Dániel/0000-0002-2912-028X\",\"url_pdf\":\"https://leventebajczi.github.io/publications/tacas25theta.pdf\",\"url_poster\":\"https://leventebajczi.github.io/publications/posters/tacas25.pdf\",\"url_mtmt\":\"https://m2.mtmt.hu/api/publication/36122885\",\"bibtex\":\"@article{MTMT:36122885,\\n\\ttitle = {Theta: Various Approaches for Concurrent Program Verification (Competition Contribution)},\\n\\tauthor = {Telbisz, Csanád Ferenc and Bajczi, Levente and Szekeres, Dániel and Vörös, András},\\n\\tdoi = {10.1007/978-3-031-90660-2_22},\\n\\tjournal-iso = {LNCS},\\n\\tjournal = {LECTURE NOTES IN COMPUTER SCIENCE},\\n\\tvolume = {15698},\\n\\tunique-id = {36122885},\\n\\tissn = {0302-9743},\\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 2025, we complement our existing approach (abstraction-aware partial order reduction) for multi-threaded programs with a happens before propagator-based BMC check, expecting a significant increase in performance. We again utilize our portfolio with dynamic algorithm selection from last year, with improvements regarding solver choice and configuration ordering. In this paper, we detail our algorithmic improvements in Theta regarding the verification of concurrent software.},\\n\\tyear = {2025},\\n\\teissn = {1611-3349},\\n\\tpages = {260-265},\\n\\torcid-numbers = {Telbisz, Csanád Ferenc/0000-0002-6260-5908; Bajczi, Levente/0000-0002-6551-5860; Szekeres, Dániel/0000-0002-2912-028X},\\n\\n\\n    url_pdf    = {https://leventebajczi.github.io/publications/tacas25theta.pdf},\\n\\turl_poster = {https://leventebajczi.github.io/publications/posters/tacas25.pdf},\\n\\turl_mtmt   = {https://m2.mtmt.hu/api/publication/36122885},\\t\\n}\\n\\n\",\"author_short\":[\"Telbisz, C. F.\",\"Bajczi, L.\",\"Szekeres, D.\",\"Vörös, A.\"],\"key\":\"MTMT:36122885\",\"id\":\"MTMT:36122885\",\"bibbaseid\":\"telbisz-bajczi-szekeres-vrs-thetavariousapproachesforconcurrentprogramverificationcompetitioncontribution-2025\",\"role\":\"author\",\"urls\":{\" pdf\":\"https://leventebajczi.github.io/publications/tacas25theta.pdf\",\" poster\":\"https://leventebajczi.github.io/publications/posters/tacas25.pdf\",\" mtmt\":\"https://m2.mtmt.hu/api/publication/36122885\"},\"metadata\":{\"authorlinks\":{\"bajczi, l\":\"https://leventebajczi.com/publications.html\"}},\"html\":\"\"},{\"bibtype\":\"article\",\"type\":\"article\",\"title\":\"SV-COMP’25 Reproduction Report (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\":[]}],\"doi\":\"10.1007/978-3-031-90660-2_10\",\"journal-iso\":\"LNCS\",\"journal\":\"LECTURE NOTES IN COMPUTER SCIENCE\",\"volume\":\"15698\",\"unique-id\":\"36122888\",\"issn\":\"0302-9743\",\"abstract\":\"The International Competition on Software Verification (SV-COMP) has been an important driver of progress in the formal verification community, fostering tool development, benchmarking, and reproducibility. As the competition grows in scale and complexity, a reproducibility study is essential to evaluate its robustness across environments, uncover hidden dependencies, and ensure long-term sustainability. This work aims to reaffirm the reliability of SV-COMP’s results, provide insights for similar competitions, and facilitate the adoption of its infrastructure beyond the competition. We reproduced the verification and validation results of active participants, including score and ranking calculations for the verification track. We found several problems prohibiting reusability and reproducibility of some participating tools, but we did not find serious issues with the competition infrastructure itself.\",\"year\":\"2025\",\"eissn\":\"1611-3349\",\"pages\":\"187-191\",\"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/tacas25repro.pdf\",\"url_slides\":\"https://leventebajczi.github.io/publications/slides/tacas25repro.pdf\",\"url_mtmt\":\"https://m2.mtmt.hu/api/publication/36122888\",\"bibtex\":\"@article{MTMT:36122888,\\n\\ttitle = {SV-COMP’25 Reproduction Report (Competition Contribution)},\\n\\tauthor = {Bajczi, Levente and Ádám, Zsófia and Micskei, Zoltán Imre},\\n\\tdoi = {10.1007/978-3-031-90660-2_10},\\n\\tjournal-iso = {LNCS},\\n\\tjournal = {LECTURE NOTES IN COMPUTER SCIENCE},\\n\\tvolume = {15698},\\n\\tunique-id = {36122888},\\n\\tissn = {0302-9743},\\n\\tabstract = {The International Competition on Software Verification (SV-COMP) has been an important driver of progress in the formal verification community, fostering tool development, benchmarking, and reproducibility. As the competition grows in scale and complexity, a reproducibility study is essential to evaluate its robustness across environments, uncover hidden dependencies, and ensure long-term sustainability. This work aims to reaffirm the reliability of SV-COMP’s results, provide insights for similar competitions, and facilitate the adoption of its infrastructure beyond the competition. We reproduced the verification and validation results of active participants, including score and ranking calculations for the verification track. We found several problems prohibiting reusability and reproducibility of some participating tools, but we did not find serious issues with the competition infrastructure itself.},\\n\\tyear = {2025},\\n\\teissn = {1611-3349},\\n\\tpages = {187-191},\\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\\n    url_pdf    = {https://leventebajczi.github.io/publications/tacas25repro.pdf},\\n\\turl_slides = {https://leventebajczi.github.io/publications/slides/tacas25repro.pdf},\\n\\turl_mtmt   = {https://m2.mtmt.hu/api/publication/36122888},\\t\\n}\\n\\n\",\"author_short\":[\"Bajczi, L.\",\"Ádám, Z.\",\"Micskei, Z. I.\"],\"key\":\"MTMT:36122888\",\"id\":\"MTMT:36122888\",\"bibbaseid\":\"bajczi-dm-micskei-svcomp25reproductionreportcompetitioncontribution-2025\",\"role\":\"author\",\"urls\":{\" pdf\":\"https://leventebajczi.github.io/publications/tacas25repro.pdf\",\" slides\":\"https://leventebajczi.github.io/publications/slides/tacas25repro.pdf\",\" mtmt\":\"https://m2.mtmt.hu/api/publication/36122888\"},\"metadata\":{\"authorlinks\":{\"bajczi, l\":\"https://leventebajczi.com/publications.html\"}},\"html\":\"\"},{\"bibtype\":\"article\",\"type\":\"article\",\"title\":\"EmergenTheta: Variations on Symbolic Transition Systems (Competition Contribution)\",\"author\":[{\"propositions\":[],\"lastnames\":[\"Mondok\"],\"firstnames\":[\"Milán\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Bajczi\"],\"firstnames\":[\"Levente\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Szekeres\"],\"firstnames\":[\"Dániel\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Molnár\"],\"firstnames\":[\"Vince\"],\"suffixes\":[]}],\"doi\":\"10.1007/978-3-031-90660-2_15\",\"journal-iso\":\"LNCS\",\"journal\":\"LECTURE NOTES IN COMPUTER SCIENCE\",\"volume\":\"15698\",\"unique-id\":\"36122891\",\"issn\":\"0302-9743\",\"abstract\":\"EmergenTheta is our sandbox for experimental analyses. After its successful debut in SV-COMP’24, we kept some well-performing but still under-tested configurations, and complemented them with a new saturation algorithm over decision diagrams, and two ways of extending their verification power: wrapping them in a lightweight, counterexample-guided abstraction refinement (CEGAR) loop based on implicit predicate abstraction; and backwards traversal of the state space. All such analyses now rely on a common interface to the underlying symbolic transition system, integrating seamlessly into the existing Theta framework. Using this combination of proven analyses and novel extensions, EmergenTheta outperformed our expectations in SV-COMP’25.\",\"year\":\"2025\",\"eissn\":\"1611-3349\",\"pages\":\"217-222\",\"orcid-numbers\":\"Mondok, Milán/0000-0001-5396-2172; Bajczi, Levente/0000-0002-6551-5860; Szekeres, Dániel/0000-0002-2912-028X; Molnár, Vince/0000-0002-8204-7595\",\"url_pdf\":\"https://leventebajczi.github.io/publications/tacas25etheta.pdf\",\"url_slides\":\"https://leventebajczi.github.io/publications/slides/tacas25etheta.pdf\",\"url_mtmt\":\"https://m2.mtmt.hu/api/publication/36122891\",\"bibtex\":\"@article{MTMT:36122891,\\n\\ttitle = {{EmergenTheta: Variations on Symbolic Transition Systems (Competition Contribution)}},\\n\\tauthor = {Mondok, Milán and Bajczi, Levente and Szekeres, Dániel and Molnár, Vince},\\n\\tdoi = {10.1007/978-3-031-90660-2_15},\\n\\tjournal-iso = {LNCS},\\n\\tjournal = {LECTURE NOTES IN COMPUTER SCIENCE},\\n\\tvolume = {15698},\\n\\tunique-id = {36122891},\\n\\tissn = {0302-9743},\\n\\tabstract = {EmergenTheta is our sandbox for experimental analyses. After its successful debut in SV-COMP’24, we kept some well-performing but still under-tested configurations, and complemented them with a new saturation algorithm over decision diagrams, and two ways of extending their verification power: wrapping them in a lightweight, counterexample-guided abstraction refinement (CEGAR) loop based on implicit predicate abstraction; and backwards traversal of the state space. All such analyses now rely on a common interface to the underlying symbolic transition system, integrating seamlessly into the existing Theta framework. Using this combination of proven analyses and novel extensions, EmergenTheta outperformed our expectations in SV-COMP’25.},\\n\\tyear = {2025},\\n\\teissn = {1611-3349},\\n\\tpages = {217-222},\\n\\torcid-numbers = {Mondok, Milán/0000-0001-5396-2172; Bajczi, Levente/0000-0002-6551-5860; Szekeres, Dániel/0000-0002-2912-028X; Molnár, Vince/0000-0002-8204-7595},\\n\\n    url_pdf    = {https://leventebajczi.github.io/publications/tacas25etheta.pdf},\\n\\turl_slides = {https://leventebajczi.github.io/publications/slides/tacas25etheta.pdf},\\n\\turl_mtmt   = {https://m2.mtmt.hu/api/publication/36122891},\\t\\n}\\n\\n\",\"author_short\":[\"Mondok, M.\",\"Bajczi, L.\",\"Szekeres, D.\",\"Molnár, V.\"],\"key\":\"MTMT:36122891\",\"id\":\"MTMT:36122891\",\"bibbaseid\":\"mondok-bajczi-szekeres-molnr-emergenthetavariationsonsymbolictransitionsystemscompetitioncontribution-2025\",\"role\":\"author\",\"urls\":{\" pdf\":\"https://leventebajczi.github.io/publications/tacas25etheta.pdf\",\" slides\":\"https://leventebajczi.github.io/publications/slides/tacas25etheta.pdf\",\" mtmt\":\"https://m2.mtmt.hu/api/publication/36122891\"},\"metadata\":{\"authorlinks\":{\"bajczi, l\":\"https://leventebajczi.com/publications.html\"}},\"html\":\"\"},{\"bibtype\":\"article\",\"type\":\"article\",\"title\":\"On Stability in a Happens-Before Propagator for Concurrent Programs (Reproducibility Study)\",\"author\":[{\"propositions\":[],\"lastnames\":[\"Bajczi\"],\"firstnames\":[\"Levente\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Telbisz\"],\"firstnames\":[\"Csanád\",\"Ferenc\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Szekeres\"],\"firstnames\":[\"Dániel\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Vörös\"],\"firstnames\":[\"András\"],\"suffixes\":[]}],\"doi\":\"10.1007/978-3-031-90643-5_1\",\"journal-iso\":\"LNCS\",\"journal\":\"LECTURE NOTES IN COMPUTER SCIENCE\",\"volume\":\"15696\",\"unique-id\":\"36122897\",\"issn\":\"0302-9743\",\"abstract\":\"Analyzing concurrent programs often involves reasoning about happens-before relations, handled by dedicated SMT theory solvers. Recently, preventative propagation rules have been introduced for consistency models to avoid unnecessary computations. This paper analyses the reproducibility of a recently published paper regarding a conflict-avoiding happens-before propagator. We show that the underlying axioms are insufficient for supporting sequential consistency. We find that the algorithm can leave out constraints on event ordering (even considering the original axioms), impacting the accuracy of verification. We show a simple counterexample to the stability claim in the paper. Two revisions of the algorithm are presented, and a proof on the correctness of these approaches respective of the original axioms is shown. The tool implementing the original algorithm is examined to ascertain how it circumvents wrong results. It is found that it deviates from the published algorithm. We show that an unmodified algorithm (via a patch in the implementing tool) causes incorrect results. We also show that our revised algorithm can be implemented efficiently in an independent verification tool.\",\"year\":\"2025\",\"eissn\":\"1611-3349\",\"pages\":\"3-19\",\"orcid-numbers\":\"Bajczi, Levente/0000-0002-6551-5860; Telbisz, Csanád Ferenc/0000-0002-6260-5908; Szekeres, Dániel/0000-0002-2912-028X\",\"url_pdf\":\"https://leventebajczi.github.io/publications/tacas25ocfix.pdf\",\"url_slides\":\"https://leventebajczi.github.io/publications/slides/tacas25ocfix.pdf\",\"url_mtmt\":\"https://m2.mtmt.hu/api/publication/36122897\",\"bibtex\":\"@article{MTMT:36122897,\\n\\ttitle = {On Stability in a Happens-Before Propagator for Concurrent Programs (Reproducibility Study)},\\n\\tauthor = {Bajczi, Levente and Telbisz, Csanád Ferenc and Szekeres, Dániel and Vörös, András},\\n\\tdoi = {10.1007/978-3-031-90643-5_1},\\n\\tjournal-iso = {LNCS},\\n\\tjournal = {LECTURE NOTES IN COMPUTER SCIENCE},\\n\\tvolume = {15696},\\n\\tunique-id = {36122897},\\n\\tissn = {0302-9743},\\n\\tabstract = {Analyzing concurrent programs often involves reasoning about happens-before relations, handled by dedicated SMT theory solvers. Recently, preventative propagation rules have been introduced for consistency models to avoid unnecessary computations. This paper analyses the reproducibility of a recently published paper regarding a conflict-avoiding happens-before propagator. We show that the underlying axioms are insufficient for supporting sequential consistency. We find that the algorithm can leave out constraints on event ordering (even considering the original axioms), impacting the accuracy of verification. We show a simple counterexample to the stability claim in the paper. Two revisions of the algorithm are presented, and a proof on the correctness of these approaches respective of the original axioms is shown. The tool implementing the original algorithm is examined to ascertain how it circumvents wrong results. It is found that it deviates from the published algorithm. We show that an unmodified algorithm (via a patch in the implementing tool) causes incorrect results. We also show that our revised algorithm can be implemented efficiently in an independent verification tool.},\\n\\tyear = {2025},\\n\\teissn = {1611-3349},\\n\\tpages = {3-19},\\n\\torcid-numbers = {Bajczi, Levente/0000-0002-6551-5860; Telbisz, Csanád Ferenc/0000-0002-6260-5908; Szekeres, Dániel/0000-0002-2912-028X},\\n\\n    url_pdf    = {https://leventebajczi.github.io/publications/tacas25ocfix.pdf},\\n\\turl_slides = {https://leventebajczi.github.io/publications/slides/tacas25ocfix.pdf},\\n\\turl_mtmt   = {https://m2.mtmt.hu/api/publication/36122897},\\t\\n}\",\"author_short\":[\"Bajczi, L.\",\"Telbisz, C. F.\",\"Szekeres, D.\",\"Vörös, A.\"],\"key\":\"MTMT:36122897\",\"id\":\"MTMT:36122897\",\"bibbaseid\":\"bajczi-telbisz-szekeres-vrs-onstabilityinahappensbeforepropagatorforconcurrentprogramsreproducibilitystudy-2025\",\"role\":\"author\",\"urls\":{\" pdf\":\"https://leventebajczi.github.io/publications/tacas25ocfix.pdf\",\" slides\":\"https://leventebajczi.github.io/publications/slides/tacas25ocfix.pdf\",\" mtmt\":\"https://m2.mtmt.hu/api/publication/36122897\"},\"metadata\":{\"authorlinks\":{\"bajczi, l\":\"https://leventebajczi.com/publications.html\"}},\"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/LiBGb3JtYWwgQW5hbHlzaXMgb2YgSGFyZHdhcmUgRmF1bHQgQWN0aXZhdGlvbnMgaW4gQ29uY3VycmVudCBFbWJlZGRlZCBTb2Z0d2FyZX0sCglhdXRob3IgPSB7QmFqY3ppLCBMZXZlbnRlIGFuZCBWw7Zyw7ZzLCBBbmRyw6FzIGFuZCBNb2xuw6FyLCBWaW5jZX0sCglkb2kgPSB7MTAuMTE0NS8zMzU4MjM4fSwKCWpvdXJuYWwtaXNvID0ge0FDTSBUIEVNQkVEIENPTVBVVCBTfSwKCWpvdXJuYWwgPSB7QUNNIFRSQU5TQUNUSU9OUyBPTiBFTUJFRERFRCBDT01QVVRJTkcgU1lTVEVNU30sCgl2b2x1bWUgPSB7MTh9LAoJdW5pcXVlLWlkID0gezMwODY1NTE1fSwKCWlzc24gPSB7MTUzOS05MDg3fSwKCWFic3RyYWN0ID0ge0Zvcm1hbCB2ZXJpZmljYXRpb24gaXMgYXBwcm9hY2hpbmcgYSBwb2ludCB3aGVyZSBpdCB3aWxsIGJlIHJlbGlhYmx5IGFwcGxpY2FibGUgdG8gZW1iZWRkZWQgc29mdHdhcmUuIEV2ZW4gdGhvdWdoIGZvcm1hbCB2ZXJpZmljYXRpb24gY2FuIGVmZmljaWVudGx5IGFuYWx5emUgbXVsdGktdGhyZWFkZWQgYXBwbGljYXRpb25zLCBtdWx0aS1jb3JlIHByb2Nlc3NvcnMgYXJlIG9mdGVuIGNvbnNpZGVyZWQgdG9vIGRhbmdlcm91cyB0byB1c2UgaW4gY3JpdGljYWwgc3lzdGVtcywgZGVzcGl0ZSB0aGUgbWFueSBiZW5lZml0cyB0aGV5IGNhbiBvZmZlci4gT25lIHJlYXNvbiBpcyB0aGUgYWR2YW5jZWQgbWVtb3J5IGNvbnNpc3RlbmN5IG1vZGVsIG9mIHN1Y2ggQ1BVcy4gTm93YWRheXMsIG1vc3Qgc29mdHdhcmUgdmVyaWZpZXJzIGFzc3VtZSBzdHJpY3Qgc2VxdWVudGlhbCBjb25zaXN0ZW5jeSwgd2hpY2ggaXMgYWxzbyB0aGUgbmHDr3ZlIHZpZXcgb2YgcHJvZ3JhbW1lcnMuIE1vZGVybiBtdWx0aS1jb3JlIHByb2Nlc3NvcnMsIGhvd2V2ZXIsIHJhcmVseSBndWFyYW50ZWUgdGhpcyBhc3N1bXB0aW9uIGJ5IGRlZmF1bHQuIEluIGFkZGl0aW9uLCBjb21wbGV4IHByb2Nlc3NvciBhcmNoaXRlY3R1cmVzIG1heSBlYXNpbHkgY29udGFpbiBkZXNpZ24gZmF1bHRzLiBUaGFua3MgdG8gdGhlIHJlY2VudCBhZHZhbmNlcyBpbiBoYXJkd2FyZSB2ZXJpZmljYXRpb24sIHRoZXNlIGZhdWx0cyBhcmUgaW5jcmVhc2luZ2x5IHZpc2libGUgYW5kIGNhbiBiZSBkZXRlY3RlZCBldmVuIGluIGV4aXN0aW5nIHByb2Nlc3NvcnMsIGdpdmluZyBhbiBvcHBvcnR1bml0eSB0byBjb21wZW5zYXRlIGZvciB0aGUgcHJvYmxlbSBpbiBzb2Z0d2FyZS4gSW4gdGhpcyBwYXBlciwgd2UgcHJvcG9zZSBhIGdlbmVyaWMgYXBwcm9hY2ggdG8gY29uc2lkZXIgaW5jb25zaXN0ZW50IGJlaGF2aW9yIG9mIHRoZSBoYXJkd2FyZSBpbiB0aGUgYW5hbHlzaXMgb2Ygc29mdHdhcmUuIE91ciBhcHByb2FjaCBpcyBiYXNlZCBvbiBmb3JtYWwgbWV0aG9kcyBhbmQgY2FuIGJlIHVzZWQgdG8gZGV0ZWN0IHRoZSBhY3RpdmF0aW9uIG9mIGV4aXN0aW5nIGhhcmR3YXJlIGZhdWx0cyBvbiB0aGUgYXBwbGljYXRpb24gbGV2ZWwgYW5kIGZhY2lsaXRhdGUgdGhlaXIgbWl0aWdhdGlvbiBpbiBzb2Z0d2FyZS4gVGhlIGFwcHJvYWNoIHJlbGllcyBoZWF2aWx5IG9uIHJlY2VudCByZXN1bHRzIG9mIG1vZGVsIGNoZWNraW5nIGFuZCBoYXJkd2FyZSB2ZXJpZmljYXRpb24gYW5kIG9mZmVycyBuZXcsIGludGVncmF0aXZlIHJlc2VhcmNoIGRpcmVjdGlvbnMuIFdlIHByb3Bvc2UgYSBwYXJ0aWFsIHNvbHV0aW9uIGJhc2VkIG9uIGV4aXN0aW5nIG1vZGVsIGNoZWNraW5nIHRvb2xzIHRvIGRlbW9uc3RyYXRlIGZlYXNpYmlsaXR5IGFuZCBldmFsdWF0ZSB0aGVpciBwZXJmb3JtYW5jZSBpbiB0aGlzIGNvbnRleHQufSwKCXllYXIgPSB7MjAxOX0sCgllaXNzbiA9IHsxNTU4LTM0NjV9LAoJb3JjaWQtbnVtYmVycyA9IHtCYWpjemksIExldmVudGUvMDAwMC0wMDAyLTY1NTEtNTg2MDsgTW9sbsOhciwgVmluY2UvMDAwMC0wMDAyLTgyMDQtNzU5NX0sCgogICAgdXJsX3BkZiAgICA9IHtodHRwczovL2xldmVudGViYWpjemkuZ2l0aHViLmlvL3B1YmxpY2F0aW9ucy9lbXNvZnQxOS5wZGZ9LAogICAgdXJsX3NsaWRlcyA9IHtodHRwczovL2xldmVudGViYWpjemkuZ2l0aHViLmlvL3B1YmxpY2F0aW9ucy9zbGlkZXMvZW1zb2Z0MTkucGRmfSwKCXVybF9tdG10ID0ge2h0dHBzOi8vbTIubXRtdC5odS9hcGkvcHVibGljYXRpb24vMzA4NjU1MTV9LAkKfQoKCgpAYXJ0aWNsZXtNVE1UOjMyODAxMDA4LAoJdGl0bGUgPSB7VGhldGE6IHBvcnRmb2xpbyBvZiBDRUdBUi1iYXNlZCBhbmFseXNlcyB3aXRoIGR5bmFtaWMgYWxnb3JpdGhtIHNlbGVjdGlvbiAoQ29tcGV0aXRpb24gQ29udHJpYnV0aW9uKX0sCglhdXRob3IgPSB7w4Fkw6FtLCBac8OzZmlhIGFuZCBCYWpjemksIExldmVudGUgYW5kIERvYm9zLUtvdsOhY3MsIE1paMOhbHkgYW5kIEhhamR1LCDDgWtvcyBhbmQgTW9sbsOhciwgVmluY2V9LAoJZG9pID0gezEwLjEwMDcvOTc4LTMtMDMwLTk5NTI3LTBfMzR9LAoJam91cm5hbC1pc28gPSB7TEVDVCBOT1RFUyBDT01QVVQgU0N9LAoJam91cm5hbCA9IHtMRUNUVVJFIE5PVEVTIElOIENPTVBVVEVSIFNDSUVOQ0V9LAoJdm9sdW1lID0gezEzMjQ0fSwKCXVuaXF1ZS1pZCA9IHszMjgwMTAwOH0sCglpc3NuID0gezAzMDItOTc0M30sCglrZXl3b3JkcyA9IHtDb21wdXRlciBTY2llbmNlLCBTb2Z0d2FyZSBFbmdpbmVlcmluZ30sCgl5ZWFyID0gezIwMjJ9LAoJZWlzc24gPSB7MTYxMS0zMzQ5fSwKCXBhZ2VzID0gezQ3NC00Nzh9LAoJb3JjaWQtbnVtYmVycyA9IHvDgWTDoW0sIFpzw7NmaWEvMDAwMC0wMDAzLTIzNTQtMTc1MDsgQmFqY3ppLCBMZXZlbnRlLzAwMDAtMDAwMi02NTUxLTU4NjA7IERvYm9zLUtvdsOhY3MsIE1paMOhbHkvMDAwMC0wMDAyLTAwNjQtMjk2NTsgSGFqZHUsIMOBa29zLzAwMDAtMDAwMS04MDAxLTg4NjU7IE1vbG7DoXIsIFZpbmNlLzAwMDAtMDAwMi04MjA0LTc1OTV9LAoJYWJzdHJhY3QgPSB7VEhFVEEgaXMgYSBtb2RlbCBjaGVja2luZyBmcmFtZXdvcmsgYmFzZWQgb24gYWJzdHJhY3Rpb24gcmVmaW5lbWVudCBhbGdvcml0aG1zLiBJbiBTVi1DT01QIDIwMjIsIHdlIGludHJvZHVjZTogMSkgcmVhc29uaW5nIGF0IHRoZSBzb3VyY2UtbGV2ZWwgdmlhIGEgZGlyZWN0IHRyYW5zbGF0aW9uIGZyb20gQyBwcm9ncmFtczsgMikgc3VwcG9ydCBmb3IgY29uY3VycmVudCBwcm9ncmFtcyB3aXRoIGludGVybGVhdmluZyBzZW1hbnRpY3M7IDMpIG1pdGlnYXRpb24gZm9yIG5vbi1wcm9ncmVzc2luZyByZWZpbmVtZW50IGxvb3BzOyA0KSBzdXBwb3J0IGZvciBTTVQtTElCLWNvbXBsaWFudCBzb2x2ZXJzLiBXZSBjb21iaW5lIGFsbCBvZiB0aGUgYWZvcmVtZW50aW9uZWQgdGVjaG5pcXVlcyBpbnRvIGEgcG9ydGZvbGlvIHdpdGggZHluYW1pYyBhbGdvcml0aG0gc2VsZWN0aW9uLn0sCgogICAgdXJsX3BkZiAgICA9IHtodHRwczovL2xldmVudGViYWpjemkuZ2l0aHViLmlvL3B1YmxpY2F0aW9ucy90YWNhczIyLnBkZn0sCiAgICB1cmxfc2xpZGVzID0ge2h0dHBzOi8vbGV2ZW50ZWJhamN6aS5naXRodWIuaW8vcHVibGljYXRpb25zL3NsaWRlcy90YWNhczIyLnBkZn0sCiAgICB1cmxfcG9zdGVyID0ge2h0dHBzOi8vbGV2ZW50ZWJhamN6aS5naXRodWIuaW8vcHVibGljYXRpb25zL3Bvc3RlcnMvdGFjYXMyMi5wZGZ9LAoJdXJsX210bXQgPSB7aHR0cHM6Ly9tMi5tdG10Lmh1L2FwaS9wdWJsaWNhdGlvbi8zMjgwMTAwOH0sCn0KCgoKCkBpbnByb2NlZWRpbmdze01UTVQ6MzQ3Njg5NzIsCgl0aXRsZSA9IHtDb25jdXJyZW50V2l0bmVzczJUZXN0OiBUZXN0LUhhcm5lc3NpbmcgdGhlIFBvd2VyIG9mIENvbmN1cnJlbmN5IChDb21wZXRpdGlvbiBDb250cmlidXRpb24pfSwKCWF1dGhvciA9IHtCYWpjemksIExldmVudGUgYW5kIMOBZMOhbSwgWnPDs2ZpYSBhbmQgTWljc2tlaSwgWm9sdMOhbiBJbXJlfSwKCWJvb2t0aXRsZSA9IHtUb29scyBhbmQgQWxnb3JpdGhtcyBmb3IgdGhlIENvbnN0cnVjdGlvbiBhbmQgQW5hbHlzaXMgb2YgU3lzdGVtc30sCglkb2kgPSB7MTAuMTAwNy85NzgtMy0wMzEtNTcyNTYtMl8xNn0sCgl1bmlxdWUtaWQgPSB7MzQ3Njg5NzJ9LAoJYWJzdHJhY3QgPSB7Q29uY3VycmVudFdpdG5lc3MyVGVzdCBpcyBhIHZpb2xhdGlvbiB3aXRuZXNzIHZhbGlkYXRvciBmb3IgY29uY3VycmVudCBzb2Z0d2FyZS4gVGFraW5nIGJvdGggbm9uZGV0ZXJtaW5pc20gb2YgZGF0YSBhbmQgaW50ZXJsZWF2aW5nLWJhc2VkIG5vbmRldGVybWluaXNtIGludG8gYWNjb3VudCwgdGhlIHRvb2wgYWltcyB0byB1c2UgdGhlIG1ldGFkYXRhIGRlc2NyaWJlZCBpbiB0aGUgdmlvbGF0aW9uIHdpdG5lc3NlcyB0byBzeW50aGVzaXplIGFuIGV4ZWN1dGFibGUgdGVzdCBoYXJuZXNzLiBXaGlsZSBwbGFndWVkIGJ5IHNvbWUgaW5pdGlhbCBjaGFsbGVuZ2VzIHlldCB0byBvdmVyY29tZSwgdGhlIHZhbGlkYXRpb24gcGVyZm9ybWFuY2Ugb2YgQ29uY3VycmVudFdpdG5lc3MyVGVzdCBjb3Jyb2JvcmF0ZXMgdGhlIHVzZWZ1bG5lc3Mgb2YgdGhlIHByb3Bvc2VkIGFwcHJvYWNoLn0sCgl5ZWFyID0gezIwMjR9LAoJcGFnZXMgPSB7MzMwLTMzNH0sCglvcmNpZC1udW1iZXJzID0ge0JhamN6aSwgTGV2ZW50ZS8wMDAwLTAwMDItNjU1MS01ODYwOyDDgWTDoW0sIFpzw7NmaWEvMDAwMC0wMDAzLTIzNTQtMTc1MDsgTWljc2tlaSwgWm9sdMOhbiBJbXJlLzAwMDAtMDAwMy0xODQ2LTI2MVh9LAoKICAgIHVybF9wZGYgICAgPSB7aHR0cHM6Ly9sZXZlbnRlYmFqY3ppLmdpdGh1Yi5pby9wdWJsaWNhdGlvbnMvdGFjYXMyNGN3dC5wZGZ9LAogICAgdXJsX3NsaWRlcyA9IHtodHRwczovL2xldmVudGViYWpjemkuZ2l0aHViLmlvL3B1YmxpY2F0aW9ucy9zbGlkZXMvdGFjYXMyNGN3dC5wZGZ9LAogICAgdXJsX210bXQgPSB7aHR0cHM6Ly9tMi5tdG10Lmh1L2FwaS9wdWJsaWNhdGlvbi8zNDc2ODk3Mn0sCn0KCgoKQGlucHJvY2VlZGluZ3N7TVRNVDozNDc2ODQyOCwKCXRpdGxlID0ge1RoZXRhOiBBYnN0cmFjdGlvbiBCYXNlZCBUZWNobmlxdWVzIGZvciBWZXJpZnlpbmcgQ29uY3VycmVuY3kgKENvbXBldGl0aW9uIENvbnRyaWJ1dGlvbil9LAoJYXV0aG9yID0ge0JhamN6aSwgTGV2ZW50ZSBhbmQgVGVsYmlzeiwgQ3NhbsOhZCBhbmQgU29tb3JqYWksIE3DoXJrIGFuZCDDgWTDoW0sIFpzw7NmaWEgYW5kIERvYm9zLUtvdsOhY3MsIE1paMOhbHkgYW5kIFN6ZWtlcmVzLCBEw6FuaWVsIGFuZCBNb25kb2ssIE1pbMOhbiBhbmQgTW9sbsOhciwgVmluY2V9LAoJYm9va3RpdGxlID0ge1Rvb2xzIGFuZCBBbGdvcml0aG1zIGZvciB0aGUgQ29uc3RydWN0aW9uIGFuZCBBbmFseXNpcyBvZiBTeXN0ZW1zfSwKCWRvaSA9IHsxMC4xMDA3Lzk3OC0zLTAzMS01NzI1Ni0yXzMwfSwKCXVuaXF1ZS1pZCA9IHszNDc2ODQyOH0sCglhYnN0cmFjdCA9IHtUaGV0YSBpcyBhIG1vZGVsIGNoZWNraW5nIGZyYW1ld29yaywgd2l0aCBhIHN0cm9uZyBlbXBoYXNpcyBvbiBlZmZlY3RpdmVseSBoYW5kbGluZyBjb25jdXJyZW5jeSBpbiBzb2Z0d2FyZSB1c2luZyBhYnN0cmFjdGlvbiByZWZpbmVtZW50IGFsZ29yaXRobXMuIEluIFNWLUNPTVAgMjAyNCwgd2UgdXNlIDEpIGFuIGFic3RyYWN0aW9uLWF3YXJlIHBhcnRpYWwgb3JkZXIgcmVkdWN0aW9uOyAyKSBhIGR5bmFtaWMgc3RhdGVtZW50IHJlZHVjdGlvbiB0ZWNobmlxdWU7IGFuZCAzKSBlbmhhbmNlZCBzdXBwb3J0IGZvciBjYWxsIHN0YWNrcyB0byBoYW5kbGUgcmVjdXJzaXZlIHByb2dyYW1zLiBXZSBpbnRlZ3JhdGUgdGhlc2UgdGVjaG5pcXVlcyBpbiBhbiBpbXByb3ZlZCBhcmNoaXRlY3R1cmUgd2l0aCBpbmhlcmVudCBzdXBwb3J0IGZvciBwb3J0Zm9saW8tYmFzZWQgdmVyaWZpY2F0aW9uIHVzaW5nIGR5bmFtaWMgYWxnb3JpdGhtIHNlbGVjdGlvbiwgd2l0aCBhIGRpdmVyc2Ugc2VsZWN0aW9uIG9mIHN1cHBvcnRlZCBTTVQgc29sdmVycyBhcyB3ZWxsLiBJbiB0aGlzIHBhcGVyIHdlIGRldGFpbCB0aGUgYWR2YW5jZXMgb2YgVGhldGEgcmVnYXJkaW5nIGNvbmN1cnJlbnQgYW5kIHJlY3Vyc2l2ZSBzb2Z0d2FyZSBzdXBwb3J0Ln0sCgl5ZWFyID0gezIwMjR9LAoJcGFnZXMgPSB7NDEyLTQxN30sCglvcmNpZC1udW1iZXJzID0ge0JhamN6aSwgTGV2ZW50ZS8wMDAwLTAwMDItNjU1MS01ODYwOyBUZWxiaXN6LCBDc2Fuw6FkLzAwMDAtMDAwMi02MjYwLTU5MDg7IMOBZMOhbSwgWnPDs2ZpYS8wMDAwLTAwMDMtMjM1NC0xNzUwOyBEb2Jvcy1Lb3bDoWNzLCBNaWjDoWx5LzAwMDAtMDAwMi0wMDY0LTI5NjU7IFN6ZWtlcmVzLCBEw6FuaWVsLzAwMDAtMDAwMi0yOTEyLTAyOFg7IE1vbmRvaywgTWlsw6FuLzAwMDAtMDAwMS01Mzk2LTIxNzI7IE1vbG7DoXIsIFZpbmNlLzAwMDAtMDAwMi04MjA0LTc1OTV9LAoKICAgIHVybF9wZGYgICAgPSB7aHR0cHM6Ly9sZXZlbnRlYmFqY3ppLmdpdGh1Yi5pby9wdWJsaWNhdGlvbnMvdGFjYXMyNHRoZXRhLnBkZn0sCiAgICB1cmxfc2xpZGVzID0ge2h0dHBzOi8vbGV2ZW50ZWJhamN6aS5naXRodWIuaW8vcHVibGljYXRpb25zL3NsaWRlcy90YWNhczI0dGhldGEucGRmfSwKICAgIHVybF9tdG10ID0ge2h0dHBzOi8vbTIubXRtdC5odS9hcGkvcHVibGljYXRpb24vMzQ3Njg0Mjh9LAp9CgoKCkBpbnByb2NlZWRpbmdze01UTVQ6MzQ3Njg0MjIsCgl0aXRsZSA9IHtFbWVyZ2VuVGhldGE6IFZlcmlmaWNhdGlvbiBCZXlvbmQgQWJzdHJhY3Rpb24gUmVmaW5lbWVudCAoQ29tcGV0aXRpb24gQ29udHJpYnV0aW9uKX0sCglhdXRob3IgPSB7QmFqY3ppLCBMZXZlbnRlIGFuZCBTemVrZXJlcywgRMOhbmllbCBhbmQgTW9uZG9rLCBNaWzDoW4gYW5kIMOBZMOhbSwgWnPDs2ZpYSBhbmQgU29tb3JqYWksIE3DoXJrIGFuZCBUZWxiaXN6LCBDc2Fuw6FkIGFuZCBEb2Jvcy1Lb3bDoWNzLCBNaWjDoWx5IGFuZCBNb2xuw6FyLCBWaW5jZX0sCglib29rdGl0bGUgPSB7VG9vbHMgYW5kIEFsZ29yaXRobXMgZm9yIHRoZSBDb25zdHJ1Y3Rpb24gYW5kIEFuYWx5c2lzIG9mIFN5c3RlbXN9LAoJZG9pID0gezEwLjEwMDcvOTc4LTMtMDMxLTU3MjU2LTJfMjN9LAoJdW5pcXVlLWlkID0gezM0NzY4NDIyfSwKCWFic3RyYWN0ID0ge1RoZXRhIGlzIGEgbW9kZWwgY2hlY2tpbmcgZnJhbWV3b3JrIGNvbnZlbnRpb25hbGx5IGJhc2VkIG9uIGFic3RyYWN0aW9uIHJlZmluZW1lbnQgdGVjaG5pcXVlcy4gV2hpbGUgYWJzdHJhY3Rpb24gaXMgdXNlZnVsIGZvciBhIGxhcmdlIG51bWJlciBvZiB2ZXJpZmljYXRpb24gcHJvYmxlbXMsIHRoZSBvdmVyLXJlbGlhbmNlIG9uIHRoZSB0ZWNobmlxdWUgbGVkIHRvIFRoZXRhIGJlaW5nIHVuYWJsZSB0byBtZWFuaW5nZnVsbHkgYWRhcHQuIElkZW50aWZ5aW5nIHRoaXMgcHJvYmxlbSBpbiBwcmV2aW91cyB5ZWFycyBvZiBTVi1DT01QIGhhcyBsZWQgdXMgdG8gY3JlYXRlIEVtZXJnZW5UaGV0YSAsIGEgc2FuZGJveCBmb3IgdGhlIG5ldyBhcHByb2FjaGVzIHdlIHdhbnQgVGhldGEgdG8gc3VwcG9ydC4gQnkgZGlmZmVyZW50aWF0aW5nIGJldHdlZW4gbWF0dXJlIGFuZCBlbWVyZ2luZyB0ZWNobmlxdWVzLCB3ZSBjYW4gZXhwZXJpbWVudCBtb3JlIGZyZWVseSB3aXRob3V0IGh1cnRpbmcgdGhlIHJlbGlhYmlsaXR5IG9mIHRoZSBvdmVyYWxsIGZyYW1ld29yay4gSW4gdGhpcyBwYXBlciB3ZSBkZXRhaWwgdGhlIGRldmVsb3BtZW50IHJvdXRlIHRvIEVtZXJnZW5UaGV0YSAsIGFuZCBpdHMgZmlyc3QgZGVidXQgb24gU1YtQ09NUOKAmTI0IGluIHRoZSBSZWFjaFNhZmV0eSBjYXRlZ29yeS59LAoJeWVhciA9IHsyMDI0fSwKCXBhZ2VzID0gezM3MS0zNzV9LAoJb3JjaWQtbnVtYmVycyA9IHtCYWpjemksIExldmVudGUvMDAwMC0wMDAyLTY1NTEtNTg2MDsgU3pla2VyZXMsIETDoW5pZWwvMDAwMC0wMDAyLTI5MTItMDI4WDsgTW9uZG9rLCBNaWzDoW4vMDAwMC0wMDAxLTUzOTYtMjE3Mjsgw4Fkw6FtLCBac8OzZmlhLzAwMDAtMDAwMy0yMzU0LTE3NTA7IFRlbGJpc3osIENzYW7DoWQvMDAwMC0wMDAyLTYyNjAtNTkwODsgRG9ib3MtS292w6FjcywgTWlow6FseS8wMDAwLTAwMDItMDA2NC0yOTY1OyBNb2xuw6FyLCBWaW5jZS8wMDAwLTAwMDItODIwNC03NTk1fSwKCiAgICB1cmxfcGRmICAgID0ge2h0dHBzOi8vbGV2ZW50ZWJhamN6aS5naXRodWIuaW8vcHVibGljYXRpb25zL3RhY2FzMjRldGhldGEucGRmfSwKICAgIHVybF9zbGlkZXMgPSB7aHR0cHM6Ly9sZXZlbnRlYmFqY3ppLmdpdGh1Yi5pby9wdWJsaWNhdGlvbnMvc2xpZGVzL3RhY2FzMjRldGhldGEucGRmfSwKICAgIHVybF9tdG10ID0ge2h0dHBzOi8vbTIubXRtdC5odS9hcGkvcHVibGljYXRpb24vMzQ3Njg0MjJ9LAp9CgoKCkBpbnByb2NlZWRpbmdze01UTVQ6MzU2MTc3NjEsCgl0aXRsZSA9IHtWZXJiZXNzZXJ1bmcgZGVyIE1CU0UtQXVzYmlsZHVuZyBkdXJjaCBWZXJzaW9uc2tvbnRyb2xsZSB1bmQgYXV0b21hdGlzaWVydGVzIEZlZWRiYWNrfSwKCWF1dGhvciA9IHtCYWpjemksIExldmVudGUgYW5kIFN6ZWtlcmVzLCBEw6FuaWVsIGFuZCBTaWVnbCwgRGFuaWVsIGFuZCBNb2xuw6FyLCBWaW5jZX0sCglib29rdGl0bGUgPSB7VGFnIGRlcyBTeXN0ZW1zIEVuZ2luZWVyaW5nfSwKCXVuaXF1ZS1pZCA9IHszNTYxNzc2MX0sCgl5ZWFyID0gezIwMjR9LAoJcGFnZXMgPSB7MTYxLTE2OX0sCglvcmNpZC1udW1iZXJzID0ge0JhamN6aSwgTGV2ZW50ZS8wMDAwLTAwMDItNjU1MS01ODYwOyBTemVrZXJlcywgRMOhbmllbC8wMDAwLTAwMDItMjkxMi0wMjhYOyBNb2xuw6FyLCBWaW5jZS8wMDAwLTAwMDItODIwNC03NTk1fSwKCiAgICB1cmxfcGRmICAgID0ge2h0dHBzOi8vbGV2ZW50ZWJhamN6aS5naXRodWIuaW8vcHVibGljYXRpb25zL3Rkc2UyNHZlcmJlc3NlcnVuZy5wZGZ9LAogICAgdXJsX3NsaWRlcyA9IHtodHRwczovL2xldmVudGViYWpjemkuZ2l0aHViLmlvL3B1YmxpY2F0aW9ucy9zbGlkZXMvdGRzZTI0dmVyYmVzc2VydW5nLnBkZn0sCiAgICB1cmxfbXRtdCA9IHtodHRwczovL20yLm10bXQuaHUvYXBpL3B1YmxpY2F0aW9uLzM1NjE3NzYxfSwKfQoKCgpAbWlzY3tiYWpjemkyMDI0ZW5oYW5jaW5nbWJzZWVkdWNhdGlvbnZlcnNpb24sCgl0aXRsZT17RW5oYW5jaW5nIE1CU0UgRWR1Y2F0aW9uIHdpdGggVmVyc2lvbiBDb250cm9sIGFuZCBBdXRvbWF0ZWQgRmVlZGJhY2t9LCAKCWF1dGhvcj17TGV2ZW50ZSBCYWpjemkgYW5kIETDoW5pZWwgU3pla2VyZXMgYW5kIERhbmllbCBTaWVnbCBhbmQgVmluY2UgTW9sbsOhcn0sCgl5ZWFyPXsyMDI0fSwKCWVwcmludD17MjQwOS4xNTI5NH0sCglhcmNoaXZlUHJlZml4PXthclhpdn0sCglwcmltYXJ5Q2xhc3M9e2NzLkNZfSwKCgl1cmxfcGRmICAgID0ge2h0dHBzOi8vbGV2ZW50ZWJhamN6aS5naXRodWIuaW8vcHVibGljYXRpb25zL3Rkc2UyNGVuaGFuY2luZy5wZGZ9LAogICAgdXJsX3NsaWRlcyA9IHtodHRwczovL2xldmVudGViYWpjemkuZ2l0aHViLmlvL3B1YmxpY2F0aW9ucy9zbGlkZXMvdGRzZTI0dmVyYmVzc2VydW5nLnBkZn0sCn0KCgoKCkBhcnRpY2xle01UTVQ6MzU3NjIxNzEsCgl0aXRsZSA9IHt7TmV0d29yQ2F0OiBhcHBseWluZyBhbmFseXNpcyB0ZWNobmlxdWVzIG9mIHNoYXJlZCBtZW1vcnkgc29mdHdhcmUgb24gbWVzc2FnZS1wYXNzaW5nIGRpc3RyaWJ1dGVkIHN5c3RlbXN9fSwKCWF1dGhvciA9IHtCYWpjemksIExldmVudGUgYW5kIE1vbG7DoXIsIFZpbmNlfSwKCWRvaSA9IHsxMC4xMDA3L3MxMDI3MC0wMjQtMDEyNTgteH0sCglqb3VybmFsLWlzbyA9IHtTT0ZUVyBTWVNUIE1PREVMfSwKCWpvdXJuYWwgPSB7U09GVFdBUkUgQU5EIFNZU1RFTVMgTU9ERUxJTkd9LAoJdW5pcXVlLWlkID0gezM1NzYyMTcxfSwKCWlzc24gPSB7MTYxOS0xMzY2fSwKCWFic3RyYWN0ID0ge0NvbW11bmljYXRpb24gbW9kZWxzIGFyZSBhIGtleSBhc3BlY3QgaW4gdGhlIGRlc2lnbiBhbmQgaW1wbGVtZW50YXRpb24gb2YgZGlzdHJpYnV0ZWQgc3lzdGVtIGFyY2hpdGVjdHVyZXMuIEFwcGxpY2F0aW9uIGxvZ2ljIG11c3QgY29uc2lkZXIgdGhlIGd1YXJhbnRlZXMgb2YgdGhlc2UgbW9kZWxzLCB3aGljaCBmdW5kYW1lbnRhbGx5IGluZmx1ZW5jZSBpdHMgY29ycmVjdG5lc3MuIE1vZGVybiBtdWx0aS1jb3JlIHByb2Nlc3NvciBhcmNoaXRlY3R1cmVzIGZhY2UgYSBzaW1pbGFyIHByb2JsZW0gd2hlbiBpdCBjb21lcyB0byBhY2Nlc3Npbmcgc2hhcmVkIG1lbW9yeTogdGhlIGd1YXJhbnRlZXMgb2YgYW4gYXJjaGl0ZWN0dXJlIGhhdmUgYSBmdW5kYW1lbnRhbCBpbXBhY3Qgb24gdGhlIG9ic2VydmFibGUgYmVoYXZpb3Igb2Ygc29mdHdhcmUuIFRoZSBmb3JtYWxpemF0aW9uIG9mIHRoZXNlIGd1YXJhbnRlZXMgaW4gYSBkZWNsYXJhdGl2ZSB3YXkgaGFzIGxlZCB0byBwb3dlcmZ1bCB0b29scyBhbmQgYWxnb3JpdGhtcyB0byBkZWZpbmUgcmV1c2FibGUgY29uc3RyYWludHMgb24gcGF0dGVybnMgb2YgbWVtb3J5IGFjY2VzcyBldmVudHMgYW5kIHRoZWlyIHJlbGF0aW9uc2hpcHMsIGVuYWJsaW5nIHRoZSBlZmZpY2llbnQgZGVzY3JpcHRpb24gYW5kIGF1dG9tYXRpYyBmb3JtYWwgYW5hbHlzaXMgb2Ygc29mdHdhcmUgcHJvcGVydGllcyB3aXRoIHJlc3BlY3QgdG8gYSBzcGVjaWZpYyBhcmNoaXRlY3R1cmUuIFRoZSBDYXQgbWVtb3J5IG1vZGVsaW5nIGxhbmd1YWdlIHByb3ZpZGVzIGEgc3RhbmRhcmQgbWVhbnMgb2Ygc3BlY2lmeWluZyB0aGVzZSBjb25zdHJhaW50cy4gRGVzcGl0ZSB0aGUgcGFyYWxsZWxzLCB0aGUgYXhpb21hdGljIG1vZGVsaW5nIGFuZCBhbmFseXNpcyBvZiBjb21tdW5pY2F0aW9uIG1vZGVscyBpbiBkaXN0cmlidXRlZCBzeXN0ZW1zIHJlbWFpbiBhIHJlbGF0aXZlbHkgdW5leHBsb3JlZCBhcmVhLiBJbiB0aGlzIHBhcGVyLCB3ZSBhZGRyZXNzIHRoaXMgZ2FwIGFuZCBkZW1vbnN0cmF0ZSBob3cgY29tbXVuaWNhdGlvbiBtb2RlbHMgY2FuIGJlIG1hcHBlZCB0byB0aGUgQ2F0IGxhbmd1YWdlLiBXZSBjcmVhdGUgYSBzdGFuZGFyZCBsaWJyYXJ5IG9mIHJldXNhYmxlIHBhdHRlcm5zIGFuZCBkZW1vbnN0cmF0ZSBvdXIgYXBwcm9hY2gsIGNhbGxlZCBOZXR3b3JDYXQgLCBvbiB0aGUgc2ltcGxlIGV4YW1wbGVzIG9mIFVEUCBhbmQgVENQLCBhbmQgd2UgYWxzbyBwcmVzZW50IGl0cyBhcHBsaWNhYmlsaXR5IHRvIHRoZSB2YXN0bHkgY29uZmlndXJhYmxlIE9NRy1ERFMgc2VydmljZS4gVGhpcyBhZGFwdGF0aW9uLWJhc2VkIGFwcHJvYWNoIGVuYWJsZXMgdGhlIHVzZSBvZiBldmVyLWltcHJvdmluZyB2ZXJpZmljYXRpb24gdG9vbHMgYnVpbHQgZm9yIHNoYXJlZCBtZW1vcnkgY29uY3VycmVuY3kgb24gZGlzdHJpYnV0ZWQgc3lzdGVtcy4gV2UgYmVsaWV2ZSB0aGlzIG5vdCBvbmx5IGJlbmVmaXRzIGRpc3RyaWJ1dGVkIHN5c3RlbSBhbmFseXNlcyBieSBicm9hZGVuaW5nIHRoZSB0b29sc2V0IGZvciB2ZXJpZmljYXRpb24gYnV0IGFsc28gcG9zaXRpdmVseSBpbXBhY3RzIHRoZSBmaWVsZCBvZiBtZW1vcnktbW9kZWwtYXdhcmUgdmVyaWZpY2F0aW9uIGJ5IHdpZGVuaW5nIGl0cyBhdWRpZW5jZSB0byBhbm90aGVyIGRvbWFpbi59LAoJeWVhciA9IHsyMDI1fSwKCWVpc3NuID0gezE2MTktMTM3NH0sCglvcmNpZC1udW1iZXJzID0ge0JhamN6aSwgTGV2ZW50ZS8wMDAwLTAwMDItNjU1MS01ODYwOyBNb2xuw6FyLCBWaW5jZS8wMDAwLTAwMDItODIwNC03NTk1fSwKCiAgICB1cmxfcGRmICAgID0ge2h0dHBzOi8vbGV2ZW50ZWJhamN6aS5naXRodWIuaW8vcHVibGljYXRpb25zL3Nvc3ltMjVuZXR3b3JjYXQucGRmfSwKCXVybF9tdG10ICAgPSB7aHR0cHM6Ly9tMi5tdG10Lmh1L2FwaS9wdWJsaWNhdGlvbi8zNTc2MjE3MX0sCn0KCgoKQGFydGljbGV7TVRNVDozMzc4NDI4MywKCXRpdGxlID0ge0JvdHRvbXMgVXAgZm9yIENIQ3M6IE5vdmVsIFRyYW5zZm9ybWF0aW9uIG9mIExpbmVhciBDb25zdHJhaW5lZCBIb3JuIENsYXVzZXMgdG8gU29mdHdhcmUgVmVyaWZpY2F0aW9ufSwKCWF1dGhvciA9IHtTb21vcmphaSwgTcOhcmsgYW5kIERvYm9zLUtvdsOhY3MsIE1paMOhbHkgYW5kIMOBZMOhbSwgWnPDs2ZpYSBhbmQgQmFqY3ppLCBMZXZlbnRlIGFuZCBWw7Zyw7ZzLCBBbmRyw6FzfSwKCWRvaSA9IHsxMC40MjA0L0VQVENTLjQwMi4xMX0sCglqb3VybmFsLWlzbyA9IHtFTEVDVFJPTiBQUk9DIFRIRU9SIENPTVBVVCBTQ0l9LAoJam91cm5hbCA9IHtFTEVDVFJPTklDIFBST0NFRURJTkdTIElOIFRIRU9SRVRJQ0FMIENPTVBVVEVSIFNDSUVOQ0V9LAoJdm9sdW1lID0gezQwMn0sCgl1bmlxdWUtaWQgPSB7MzM3ODQyODN9LAoJYWJzdHJhY3QgPSB7Q29uc3RyYWluZWQgSG9ybiBDbGF1c2VzIChDSENzKSBoYXZlIGNvbnZlbnRpb25hbGx5IGJlZW4gdXNlZCBhcyBhIGxvdy1sZXZlbCByZXByZXNlbnRhdGlvbiBpbiBmb3JtYWwgdmVyaWZpY2F0aW9uLiBNb3N0IGV4aXN0aW5nIHNvbHZlcnMgdXNlIGEgZGl2ZXJzZSBzZXQgb2Ygc3BlY2lhbGl6ZWQgdGVjaG5pcXVlcywgaW5jbHVkaW5nIGRpcmVjdCBzdGF0ZSBzcGFjZSB0cmF2ZXJzYWwgb3IgdW5kZXItYXBwcm94aW1hdGluZyBhYnN0cmFjdGlvbiwgbmVjZXNzaXRhdGluZyBwdXJwb3NlLWJ1aWx0IGNvbXBsZXggYWxnb3JpdGhtcy4gT3RoZXIgc29sdmVycyBzdWNjZXNzZnVsbHkgc2ltcGxpZmllZCB0aGUgdmVyaWZpY2F0aW9uIHdvcmtmbG93IGJ5IHRyYW5zbGF0aW5nIHRoZSBwcm9ibGVtIHRvIGlucHV0cyBmb3Igb3RoZXIgdmVyaWZpY2F0aW9uIHRhc2tzLCBsZXZlcmFnaW5nIHRoZSBzdHJlbmd0aHMgb2YgZXhpc3RpbmcgYWxnb3JpdGhtcy4gT25lIHN1Y2ggYXBwcm9hY2ggdHJhbnNmb3JtcyB0aGUgQ0hDIHByb2JsZW0gaW50byBhIHJlY3Vyc2l2ZSBwcm9ncmFtIHJvdWdobHkgZW11bGF0aW5nIGEgdG9wLWRvd24gc29sdmVyIGZvciB0aGUgZGVkdWN0aW9uIHRhc2s7IGFuZCB2ZXJpZnlpbmcgdGhlIHJlYWNoYWJpbGl0eSBvZiBhIHNhZmV0eSB2aW9sYXRpb24gc3BlY2lmaWVkIGFzIGEgY29udHJvbCBsb2NhdGlvbi4gV2UgcHJvcG9zZSBhbiBhbHRlcm5hdGl2ZSBib3R0b20tdXAgYXBwcm9hY2ggZm9yIGxpbmVhciBDSENzLCBhbmQgZXZhbHVhdGUgdGhlIHR3byBvcHRpb25zIGluIHRoZSBvcGVuLXNvdXJjZSBtb2RlbCBjaGVja2luZyBmcmFtZXdvcmsgVEhFVEEgb24gYm90aCBzeW50aGV0aWMgYW5kIGluZHVzdHJpYWwgZXhhbXBsZXMuIFdlIGZpbmQgdGhhdCB0aGVyZSBpcyBhIG1vcmUgdGhhbiB0d29mb2xkIGluY3JlYXNlIGluIHRoZSBudW1iZXIgb2Ygc29sdmVkIHRhc2tzIHdoZW4gdGhlIG5vdmVsIGJvdHRvbS11cCBhcHByb2FjaCBpcyB1c2VkIGluIHRoZSB2ZXJpZmljYXRpb24gd29ya2Zsb3csIGluIGNvbnRyYXN0IHdpdGggdGhlIHRvcC1kb3duIHRlY2huaXF1ZS4gwqkgTcOhcmsgU29tb3JqYWkgZXQgYWwufSwKCXllYXIgPSB7MjAyNH0sCgllaXNzbiA9IHsyMDc1LTIxODB9LAoJcGFnZXMgPSB7MTA1LTExN30sCglvcmNpZC1udW1iZXJzID0ge0RvYm9zLUtvdsOhY3MsIE1paMOhbHkvMDAwMC0wMDAyLTAwNjQtMjk2NTsgw4Fkw6FtLCBac8OzZmlhLzAwMDAtMDAwMy0yMzU0LTE3NTA7IEJhamN6aSwgTGV2ZW50ZS8wMDAwLTAwMDItNjU1MS01ODYwfSwKCiAgICB1cmxfcGRmICAgID0ge2h0dHBzOi8vbGV2ZW50ZWJhamN6aS5naXRodWIuaW8vcHVibGljYXRpb25zL2hjdnMyNGNoYy5wZGZ9LAoJdXJsX210bXQgICA9IHtodHRwczovL20yLm10bXQuaHUvYXBpL3B1YmxpY2F0aW9uLzMzNzg0MjgzfSwJCn0KCgoKQGFydGljbGV7TVRNVDozNDg1MzAzMSwKCXRpdGxlID0ge1NvbHZpbmcgQ29uc3RyYWluZWQgSG9ybiBDbGF1c2VzIGFzIEMgUHJvZ3JhbXMgd2l0aCBDSEMyQ30sCglhdXRob3IgPSB7QmFqY3ppLCBMZXZlbnRlIGFuZCBNb2xuw6FyLCBWaW5jZX0sCglkb2kgPSB7MTAuMTAwNy85NzgtMy0wMzEtNjYxNDktNV84fSwKCWpvdXJuYWwtaXNvID0ge0xOQ1N9LAoJam91cm5hbCA9IHtMRUNUVVJFIE5PVEVTIElOIENPTVBVVEVSIFNDSUVOQ0V9LAoJdm9sdW1lID0gezE0NjI0fSwKCXVuaXF1ZS1pZCA9IHszNDg1MzAzMX0sCglpc3NuID0gezAzMDItOTc0M30sCglhYnN0cmFjdCA9IHtTb2x2aW5nIENvbnN0cmFpbmVkIEhvcm4gQ2xhdXNlcyAoQ0hDKSBpcyBuZWNlc3NpdGF0ZWQgYnkgbnVtZXJvdXMgZmllbGRzIGluIGZvcm1hbCBtZXRob2RzLCBmcm9tIHZlcmlmeWluZyBzb2Z0d2FyZSBhbmQgc21hcnQgY29udHJhY3RzIHRvIG1vZGVsaW5nIHN5c3RlbXMsIHlldCB0aGUgY29tcGV0aXRpdmUgc2NlbmUgZm9yIGFjYWRlbWljIHRvb2xzIHJlbWFpbnMgZmFpcmx5IHNwYXJzZSwgZXNwZWNpYWxseSBjb21wYXJlZCB0byBtb3JlIHBvcHVsYXIgZmllbGRzIHN1Y2ggYXMgc29mdHdhcmUgdmVyaWZpY2F0aW9uLiBDb21wYXJhdGl2ZSBldmFsdWF0aW9uIGFzIGEgY29tcGV0aXRpb24sIHN1Y2ggYXMgU1YtQ09NUCBvciBDSEMtQ09NUCwgc3BhcmtzIGEgbW9yZSBjb2hlc2l2ZSBjb21tdW5pdHkgYXJvdW5kIGZpZWxkcyBpbiBmb3JtYWwgbWV0aG9kcy4gTGF0ZWx5LCBhIHRyZW5kIGhhcyBiZWVuIGVtZXJnaW5nIHdpdGggdG9vbHMgc3VjaCBhcyBCdG9yMkMgdGhhdCBicmlkZ2UgbXVsdGlwbGUgZmllbGRzIHRvZ2V0aGVyLCB0aHVzIHdpZGVuaW5nIHRoaXMgY29oZXNpb24uIEZvbGxvd2luZyB0aGF0IGV4YW1wbGUsIHdlIHByb3Bvc2UgYW5kIHBlcmZvcm0gYW4gZXhwZXJpbWVudCwgd2hlcmUgd2UgdXNlIENIQy10by1DIHRyYW5zZm9ybWF0aW9uIHRvIGFwcGx5IHNvZnR3YXJlIHZlcmlmaWNhdGlvbiB0b29scyB0byBsaW5lYXIgQ0hDIHByb2JsZW1zLiBJbiB0aGUgcHJvY2Vzcywgd2UgaGVscCBib3RoIGZpZWxkcyBieSBkaXZlcnNpZnlpbmcgdGhlIHNjZW5lIG9mIENIQyBzb2x2ZXJzIGFuZCBwcm92aWRpbmcgbmV3IGFuZCB2YWx1YWJsZSBiZW5jaG1hcmtzIHRvIGFpZCB0aGUgZGV2ZWxvcG1lbnQgb2Ygc29mdHdhcmUgdmVyaWZpY2F0aW9uIHRvb2xzLiBVc2luZyB0aGVzZSBiZW5jaG1hcmtzLCB3ZSB1bmNvdmVyZWQgYSBwcmV2aW91c2x5IGhpZGRlbiBidWcgaW4gbXVsdGlwbGUgdmVyaWZpY2F0aW9uIHRvb2xzIHRoYXQgY2FuIGxlYWQgdG8gZmFsc2UgcG9zaXRpdmUgcmVzdWx0cy4gQnkgYW5hbHlzaW5nIHRoZSByZXN1bHRzIG9mIHRoZSBleHBlcmltZW50LCB3ZSBjYW4gY29uZmlkZW50bHkgbWFrZSBhIHJlY29tbWVuZGF0aW9uIGZvciBkZXZlbG9wZXJzIG9mIHNvZnR3YXJlIHZlcmlmaWVycyB0byBjb25zaWRlciBzdXBwb3J0aW5nIENIQ3MgdmlhIG91ciBwcmUtdmVyaWZpY2F0aW9uIHRyYW5zZm9ybWF0aW9uLn0sCglrZXl3b3JkcyA9IHt2ZXJpZmljYXRpb247IGZvcm1hbCBtZXRob2RzOyBDb21wdXRlciBTY2llbmNlLCBTb2Z0d2FyZSBFbmdpbmVlcmluZzsgQ0hDfSwKCXllYXIgPSB7MjAyNH0sCgllaXNzbiA9IHsxNjExLTMzNDl9LAoJcGFnZXMgPSB7MTQ2LTE2M30sCglvcmNpZC1udW1iZXJzID0ge0JhamN6aSwgTGV2ZW50ZS8wMDAwLTAwMDItNjU1MS01ODYwOyBNb2xuw6FyLCBWaW5jZS8wMDAwLTAwMDItODIwNC03NTk1fSwKCgogICAgdXJsX3BkZiAgICA9IHtodHRwczovL2xldmVudGViYWpjemkuZ2l0aHViLmlvL3B1YmxpY2F0aW9ucy9zcGluMjRjaGMyYy5wZGZ9LAogICAgdXJsX3NsaWRlcyA9IHtodHRwczovL2xldmVudGViYWpjemkuZ2l0aHViLmlvL3B1YmxpY2F0aW9ucy9zbGlkZXMvc3BpbjI0Y2hjMmMucGRmfSwKCXVybF9tdG10ICAgPSB7aHR0cHM6Ly9tMi5tdG10Lmh1L2FwaS9wdWJsaWNhdGlvbi8zNDg1MzAzMX0sCQp9CgoKCkBhcnRpY2xle01UTVQ6MzYxMjI4ODUsCgl0aXRsZSA9IHtUaGV0YTogVmFyaW91cyBBcHByb2FjaGVzIGZvciBDb25jdXJyZW50IFByb2dyYW0gVmVyaWZpY2F0aW9uIChDb21wZXRpdGlvbiBDb250cmlidXRpb24pfSwKCWF1dGhvciA9IHtUZWxiaXN6LCBDc2Fuw6FkIEZlcmVuYyBhbmQgQmFqY3ppLCBMZXZlbnRlIGFuZCBTemVrZXJlcywgRMOhbmllbCBhbmQgVsO2csO2cywgQW5kcsOhc30sCglkb2kgPSB7MTAuMTAwNy85NzgtMy0wMzEtOTA2NjAtMl8yMn0sCglqb3VybmFsLWlzbyA9IHtMTkNTfSwKCWpvdXJuYWwgPSB7TEVDVFVSRSBOT1RFUyBJTiBDT01QVVRFUiBTQ0lFTkNFfSwKCXZvbHVtZSA9IHsxNTY5OH0sCgl1bmlxdWUtaWQgPSB7MzYxMjI4ODV9LAoJaXNzbiA9IHswMzAyLTk3NDN9LAoJYWJzdHJhY3QgPSB7VGhldGEgaXMgYSBtb2RlbCBjaGVja2luZyBmcmFtZXdvcmsgd2l0aCBhIHN0cm9uZyBlbXBoYXNpcyBvbiBlZmZlY3RpdmVseSBoYW5kbGluZyBjb25jdXJyZW5jeSBpbiBzb2Z0d2FyZSB1c2luZyBhYnN0cmFjdGlvbiByZWZpbmVtZW50IGFsZ29yaXRobXMuIEluIFNWLUNPTVAgMjAyNSwgd2UgY29tcGxlbWVudCBvdXIgZXhpc3RpbmcgYXBwcm9hY2ggKGFic3RyYWN0aW9uLWF3YXJlIHBhcnRpYWwgb3JkZXIgcmVkdWN0aW9uKSBmb3IgbXVsdGktdGhyZWFkZWQgcHJvZ3JhbXMgd2l0aCBhIGhhcHBlbnMgYmVmb3JlIHByb3BhZ2F0b3ItYmFzZWQgQk1DIGNoZWNrLCBleHBlY3RpbmcgYSBzaWduaWZpY2FudCBpbmNyZWFzZSBpbiBwZXJmb3JtYW5jZS4gV2UgYWdhaW4gdXRpbGl6ZSBvdXIgcG9ydGZvbGlvIHdpdGggZHluYW1pYyBhbGdvcml0aG0gc2VsZWN0aW9uIGZyb20gbGFzdCB5ZWFyLCB3aXRoIGltcHJvdmVtZW50cyByZWdhcmRpbmcgc29sdmVyIGNob2ljZSBhbmQgY29uZmlndXJhdGlvbiBvcmRlcmluZy4gSW4gdGhpcyBwYXBlciwgd2UgZGV0YWlsIG91ciBhbGdvcml0aG1pYyBpbXByb3ZlbWVudHMgaW4gVGhldGEgcmVnYXJkaW5nIHRoZSB2ZXJpZmljYXRpb24gb2YgY29uY3VycmVudCBzb2Z0d2FyZS59LAoJeWVhciA9IHsyMDI1fSwKCWVpc3NuID0gezE2MTEtMzM0OX0sCglwYWdlcyA9IHsyNjAtMjY1fSwKCW9yY2lkLW51bWJlcnMgPSB7VGVsYmlzeiwgQ3NhbsOhZCBGZXJlbmMvMDAwMC0wMDAyLTYyNjAtNTkwODsgQmFqY3ppLCBMZXZlbnRlLzAwMDAtMDAwMi02NTUxLTU4NjA7IFN6ZWtlcmVzLCBEw6FuaWVsLzAwMDAtMDAwMi0yOTEyLTAyOFh9LAoKCiAgICB1cmxfcGRmICAgID0ge2h0dHBzOi8vbGV2ZW50ZWJhamN6aS5naXRodWIuaW8vcHVibGljYXRpb25zL3RhY2FzMjV0aGV0YS5wZGZ9LAoJdXJsX3Bvc3RlciA9IHtodHRwczovL2xldmVudGViYWpjemkuZ2l0aHViLmlvL3B1YmxpY2F0aW9ucy9wb3N0ZXJzL3RhY2FzMjUucGRmfSwKCXVybF9tdG10ICAgPSB7aHR0cHM6Ly9tMi5tdG10Lmh1L2FwaS9wdWJsaWNhdGlvbi8zNjEyMjg4NX0sCQp9CgoKCkBhcnRpY2xle01UTVQ6MzYxMjI4ODgsCgl0aXRsZSA9IHtTVi1DT01Q4oCZMjUgUmVwcm9kdWN0aW9uIFJlcG9ydCAoQ29tcGV0aXRpb24gQ29udHJpYnV0aW9uKX0sCglhdXRob3IgPSB7QmFqY3ppLCBMZXZlbnRlIGFuZCDDgWTDoW0sIFpzw7NmaWEgYW5kIE1pY3NrZWksIFpvbHTDoW4gSW1yZX0sCglkb2kgPSB7MTAuMTAwNy85NzgtMy0wMzEtOTA2NjAtMl8xMH0sCglqb3VybmFsLWlzbyA9IHtMTkNTfSwKCWpvdXJuYWwgPSB7TEVDVFVSRSBOT1RFUyBJTiBDT01QVVRFUiBTQ0lFTkNFfSwKCXZvbHVtZSA9IHsxNTY5OH0sCgl1bmlxdWUtaWQgPSB7MzYxMjI4ODh9LAoJaXNzbiA9IHswMzAyLTk3NDN9LAoJYWJzdHJhY3QgPSB7VGhlIEludGVybmF0aW9uYWwgQ29tcGV0aXRpb24gb24gU29mdHdhcmUgVmVyaWZpY2F0aW9uIChTVi1DT01QKSBoYXMgYmVlbiBhbiBpbXBvcnRhbnQgZHJpdmVyIG9mIHByb2dyZXNzIGluIHRoZSBmb3JtYWwgdmVyaWZpY2F0aW9uIGNvbW11bml0eSwgZm9zdGVyaW5nIHRvb2wgZGV2ZWxvcG1lbnQsIGJlbmNobWFya2luZywgYW5kIHJlcHJvZHVjaWJpbGl0eS4gQXMgdGhlIGNvbXBldGl0aW9uIGdyb3dzIGluIHNjYWxlIGFuZCBjb21wbGV4aXR5LCBhIHJlcHJvZHVjaWJpbGl0eSBzdHVkeSBpcyBlc3NlbnRpYWwgdG8gZXZhbHVhdGUgaXRzIHJvYnVzdG5lc3MgYWNyb3NzIGVudmlyb25tZW50cywgdW5jb3ZlciBoaWRkZW4gZGVwZW5kZW5jaWVzLCBhbmQgZW5zdXJlIGxvbmctdGVybSBzdXN0YWluYWJpbGl0eS4gVGhpcyB3b3JrIGFpbXMgdG8gcmVhZmZpcm0gdGhlIHJlbGlhYmlsaXR5IG9mIFNWLUNPTVDigJlzIHJlc3VsdHMsIHByb3ZpZGUgaW5zaWdodHMgZm9yIHNpbWlsYXIgY29tcGV0aXRpb25zLCBhbmQgZmFjaWxpdGF0ZSB0aGUgYWRvcHRpb24gb2YgaXRzIGluZnJhc3RydWN0dXJlIGJleW9uZCB0aGUgY29tcGV0aXRpb24uIFdlIHJlcHJvZHVjZWQgdGhlIHZlcmlmaWNhdGlvbiBhbmQgdmFsaWRhdGlvbiByZXN1bHRzIG9mIGFjdGl2ZSBwYXJ0aWNpcGFudHMsIGluY2x1ZGluZyBzY29yZSBhbmQgcmFua2luZyBjYWxjdWxhdGlvbnMgZm9yIHRoZSB2ZXJpZmljYXRpb24gdHJhY2suIFdlIGZvdW5kIHNldmVyYWwgcHJvYmxlbXMgcHJvaGliaXRpbmcgcmV1c2FiaWxpdHkgYW5kIHJlcHJvZHVjaWJpbGl0eSBvZiBzb21lIHBhcnRpY2lwYXRpbmcgdG9vbHMsIGJ1dCB3ZSBkaWQgbm90IGZpbmQgc2VyaW91cyBpc3N1ZXMgd2l0aCB0aGUgY29tcGV0aXRpb24gaW5mcmFzdHJ1Y3R1cmUgaXRzZWxmLn0sCgl5ZWFyID0gezIwMjV9LAoJZWlzc24gPSB7MTYxMS0zMzQ5fSwKCXBhZ2VzID0gezE4Ny0xOTF9LAoJb3JjaWQtbnVtYmVycyA9IHtCYWpjemksIExldmVudGUvMDAwMC0wMDAyLTY1NTEtNTg2MDsgw4Fkw6FtLCBac8OzZmlhLzAwMDAtMDAwMy0yMzU0LTE3NTA7IE1pY3NrZWksIFpvbHTDoW4gSW1yZS8wMDAwLTAwMDMtMTg0Ni0yNjFYfSwKCgogICAgdXJsX3BkZiAgICA9IHtodHRwczovL2xldmVudGViYWpjemkuZ2l0aHViLmlvL3B1YmxpY2F0aW9ucy90YWNhczI1cmVwcm8ucGRmfSwKCXVybF9zbGlkZXMgPSB7aHR0cHM6Ly9sZXZlbnRlYmFqY3ppLmdpdGh1Yi5pby9wdWJsaWNhdGlvbnMvc2xpZGVzL3RhY2FzMjVyZXByby5wZGZ9LAoJdXJsX210bXQgICA9IHtodHRwczovL20yLm10bXQuaHUvYXBpL3B1YmxpY2F0aW9uLzM2MTIyODg4fSwJCn0KCgoKQGFydGljbGV7TVRNVDozNjEyMjg5MSwKCXRpdGxlID0ge3tFbWVyZ2VuVGhldGE6IFZhcmlhdGlvbnMgb24gU3ltYm9saWMgVHJhbnNpdGlvbiBTeXN0ZW1zIChDb21wZXRpdGlvbiBDb250cmlidXRpb24pfX0sCglhdXRob3IgPSB7TW9uZG9rLCBNaWzDoW4gYW5kIEJhamN6aSwgTGV2ZW50ZSBhbmQgU3pla2VyZXMsIETDoW5pZWwgYW5kIE1vbG7DoXIsIFZpbmNlfSwKCWRvaSA9IHsxMC4xMDA3Lzk3OC0zLTAzMS05MDY2MC0yXzE1fSwKCWpvdXJuYWwtaXNvID0ge0xOQ1N9LAoJam91cm5hbCA9IHtMRUNUVVJFIE5PVEVTIElOIENPTVBVVEVSIFNDSUVOQ0V9LAoJdm9sdW1lID0gezE1Njk4fSwKCXVuaXF1ZS1pZCA9IHszNjEyMjg5MX0sCglpc3NuID0gezAzMDItOTc0M30sCglhYnN0cmFjdCA9IHtFbWVyZ2VuVGhldGEgaXMgb3VyIHNhbmRib3ggZm9yIGV4cGVyaW1lbnRhbCBhbmFseXNlcy4gQWZ0ZXIgaXRzIHN1Y2Nlc3NmdWwgZGVidXQgaW4gU1YtQ09NUOKAmTI0LCB3ZSBrZXB0IHNvbWUgd2VsbC1wZXJmb3JtaW5nIGJ1dCBzdGlsbCB1bmRlci10ZXN0ZWQgY29uZmlndXJhdGlvbnMsIGFuZCBjb21wbGVtZW50ZWQgdGhlbSB3aXRoIGEgbmV3IHNhdHVyYXRpb24gYWxnb3JpdGhtIG92ZXIgZGVjaXNpb24gZGlhZ3JhbXMsIGFuZCB0d28gd2F5cyBvZiBleHRlbmRpbmcgdGhlaXIgdmVyaWZpY2F0aW9uIHBvd2VyOiB3cmFwcGluZyB0aGVtIGluIGEgbGlnaHR3ZWlnaHQsIGNvdW50ZXJleGFtcGxlLWd1aWRlZCBhYnN0cmFjdGlvbiByZWZpbmVtZW50IChDRUdBUikgbG9vcCBiYXNlZCBvbiBpbXBsaWNpdCBwcmVkaWNhdGUgYWJzdHJhY3Rpb247IGFuZCBiYWNrd2FyZHMgdHJhdmVyc2FsIG9mIHRoZSBzdGF0ZSBzcGFjZS4gQWxsIHN1Y2ggYW5hbHlzZXMgbm93IHJlbHkgb24gYSBjb21tb24gaW50ZXJmYWNlIHRvIHRoZSB1bmRlcmx5aW5nIHN5bWJvbGljIHRyYW5zaXRpb24gc3lzdGVtLCBpbnRlZ3JhdGluZyBzZWFtbGVzc2x5IGludG8gdGhlIGV4aXN0aW5nIFRoZXRhIGZyYW1ld29yay4gVXNpbmcgdGhpcyBjb21iaW5hdGlvbiBvZiBwcm92ZW4gYW5hbHlzZXMgYW5kIG5vdmVsIGV4dGVuc2lvbnMsIEVtZXJnZW5UaGV0YSBvdXRwZXJmb3JtZWQgb3VyIGV4cGVjdGF0aW9ucyBpbiBTVi1DT01Q4oCZMjUufSwKCXllYXIgPSB7MjAyNX0sCgllaXNzbiA9IHsxNjExLTMzNDl9LAoJcGFnZXMgPSB7MjE3LTIyMn0sCglvcmNpZC1udW1iZXJzID0ge01vbmRvaywgTWlsw6FuLzAwMDAtMDAwMS01Mzk2LTIxNzI7IEJhamN6aSwgTGV2ZW50ZS8wMDAwLTAwMDItNjU1MS01ODYwOyBTemVrZXJlcywgRMOhbmllbC8wMDAwLTAwMDItMjkxMi0wMjhYOyBNb2xuw6FyLCBWaW5jZS8wMDAwLTAwMDItODIwNC03NTk1fSwKCiAgICB1cmxfcGRmICAgID0ge2h0dHBzOi8vbGV2ZW50ZWJhamN6aS5naXRodWIuaW8vcHVibGljYXRpb25zL3RhY2FzMjVldGhldGEucGRmfSwKCXVybF9zbGlkZXMgPSB7aHR0cHM6Ly9sZXZlbnRlYmFqY3ppLmdpdGh1Yi5pby9wdWJsaWNhdGlvbnMvc2xpZGVzL3RhY2FzMjVldGhldGEucGRmfSwKCXVybF9tdG10ICAgPSB7aHR0cHM6Ly9tMi5tdG10Lmh1L2FwaS9wdWJsaWNhdGlvbi8zNjEyMjg5MX0sCQp9CgoKCkBhcnRpY2xle01UTVQ6MzYxMjI4OTcsCgl0aXRsZSA9IHtPbiBTdGFiaWxpdHkgaW4gYSBIYXBwZW5zLUJlZm9yZSBQcm9wYWdhdG9yIGZvciBDb25jdXJyZW50IFByb2dyYW1zIChSZXByb2R1Y2liaWxpdHkgU3R1ZHkpfSwKCWF1dGhvciA9IHtCYWpjemksIExldmVudGUgYW5kIFRlbGJpc3osIENzYW7DoWQgRmVyZW5jIGFuZCBTemVrZXJlcywgRMOhbmllbCBhbmQgVsO2csO2cywgQW5kcsOhc30sCglkb2kgPSB7MTAuMTAwNy85NzgtMy0wMzEtOTA2NDMtNV8xfSwKCWpvdXJuYWwtaXNvID0ge0xOQ1N9LAoJam91cm5hbCA9IHtMRUNUVVJFIE5PVEVTIElOIENPTVBVVEVSIFNDSUVOQ0V9LAoJdm9sdW1lID0gezE1Njk2fSwKCXVuaXF1ZS1pZCA9IHszNjEyMjg5N30sCglpc3NuID0gezAzMDItOTc0M30sCglhYnN0cmFjdCA9IHtBbmFseXppbmcgY29uY3VycmVudCBwcm9ncmFtcyBvZnRlbiBpbnZvbHZlcyByZWFzb25pbmcgYWJvdXQgaGFwcGVucy1iZWZvcmUgcmVsYXRpb25zLCBoYW5kbGVkIGJ5IGRlZGljYXRlZCBTTVQgdGhlb3J5IHNvbHZlcnMuIFJlY2VudGx5LCBwcmV2ZW50YXRpdmUgcHJvcGFnYXRpb24gcnVsZXMgaGF2ZSBiZWVuIGludHJvZHVjZWQgZm9yIGNvbnNpc3RlbmN5IG1vZGVscyB0byBhdm9pZCB1bm5lY2Vzc2FyeSBjb21wdXRhdGlvbnMuIFRoaXMgcGFwZXIgYW5hbHlzZXMgdGhlIHJlcHJvZHVjaWJpbGl0eSBvZiBhIHJlY2VudGx5IHB1Ymxpc2hlZCBwYXBlciByZWdhcmRpbmcgYSBjb25mbGljdC1hdm9pZGluZyBoYXBwZW5zLWJlZm9yZSBwcm9wYWdhdG9yLiBXZSBzaG93IHRoYXQgdGhlIHVuZGVybHlpbmcgYXhpb21zIGFyZSBpbnN1ZmZpY2llbnQgZm9yIHN1cHBvcnRpbmcgc2VxdWVudGlhbCBjb25zaXN0ZW5jeS4gV2UgZmluZCB0aGF0IHRoZSBhbGdvcml0aG0gY2FuIGxlYXZlIG91dCBjb25zdHJhaW50cyBvbiBldmVudCBvcmRlcmluZyAoZXZlbiBjb25zaWRlcmluZyB0aGUgb3JpZ2luYWwgYXhpb21zKSwgaW1wYWN0aW5nIHRoZSBhY2N1cmFjeSBvZiB2ZXJpZmljYXRpb24uIFdlIHNob3cgYSBzaW1wbGUgY291bnRlcmV4YW1wbGUgdG8gdGhlIHN0YWJpbGl0eSBjbGFpbSBpbiB0aGUgcGFwZXIuIFR3byByZXZpc2lvbnMgb2YgdGhlIGFsZ29yaXRobSBhcmUgcHJlc2VudGVkLCBhbmQgYSBwcm9vZiBvbiB0aGUgY29ycmVjdG5lc3Mgb2YgdGhlc2UgYXBwcm9hY2hlcyByZXNwZWN0aXZlIG9mIHRoZSBvcmlnaW5hbCBheGlvbXMgaXMgc2hvd24uIFRoZSB0b29sIGltcGxlbWVudGluZyB0aGUgb3JpZ2luYWwgYWxnb3JpdGhtIGlzIGV4YW1pbmVkIHRvIGFzY2VydGFpbiBob3cgaXQgY2lyY3VtdmVudHMgd3JvbmcgcmVzdWx0cy4gSXQgaXMgZm91bmQgdGhhdCBpdCBkZXZpYXRlcyBmcm9tIHRoZSBwdWJsaXNoZWQgYWxnb3JpdGhtLiBXZSBzaG93IHRoYXQgYW4gdW5tb2RpZmllZCBhbGdvcml0aG0gKHZpYSBhIHBhdGNoIGluIHRoZSBpbXBsZW1lbnRpbmcgdG9vbCkgY2F1c2VzIGluY29ycmVjdCByZXN1bHRzLiBXZSBhbHNvIHNob3cgdGhhdCBvdXIgcmV2aXNlZCBhbGdvcml0aG0gY2FuIGJlIGltcGxlbWVudGVkIGVmZmljaWVudGx5IGluIGFuIGluZGVwZW5kZW50IHZlcmlmaWNhdGlvbiB0b29sLn0sCgl5ZWFyID0gezIwMjV9LAoJZWlzc24gPSB7MTYxMS0zMzQ5fSwKCXBhZ2VzID0gezMtMTl9LAoJb3JjaWQtbnVtYmVycyA9IHtCYWpjemksIExldmVudGUvMDAwMC0wMDAyLTY1NTEtNTg2MDsgVGVsYmlzeiwgQ3NhbsOhZCBGZXJlbmMvMDAwMC0wMDAyLTYyNjAtNTkwODsgU3pla2VyZXMsIETDoW5pZWwvMDAwMC0wMDAyLTI5MTItMDI4WH0sCgogICAgdXJsX3BkZiAgICA9IHtodHRwczovL2xldmVudGViYWpjemkuZ2l0aHViLmlvL3B1YmxpY2F0aW9ucy90YWNhczI1b2NmaXgucGRmfSwKCXVybF9zbGlkZXMgPSB7aHR0cHM6Ly9sZXZlbnRlYmFqY3ppLmdpdGh1Yi5pby9wdWJsaWNhdGlvbnMvc2xpZGVzL3RhY2FzMjVvY2ZpeC5wZGZ9LAoJdXJsX210bXQgICA9IHtodHRwczovL20yLm10bXQuaHUvYXBpL3B1YmxpY2F0aW9uLzM2MTIyODk3fSwJCn0=\">\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%3A%2F%2Fleventebajczi.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%3A%2F%2Fleventebajczi.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%3A%2F%2Fleventebajczi.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_2025\">\n    <div class=\"bibbase_group\"\n      onclick=\"toggleGroup('group_2025')\"\n      onkeypress=\"toggleGroup('group_2025')\"\n      tabindex=\"0\">\n      <i class=\"fa fa-angle-down bibbase_group_head_icon\"></i>&nbsp;\n      <span>2025</span>\n      <span class=\"bibbase_group_count\">\n        \n        (5)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\n      \n  \n  <div class=\"bibbase_paper\" id=\"bajczi-molnr-networcatapplyinganalysistechniquesofsharedmemorysoftwareonmessagepassingdistributedsystems-2025\">\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/sosym25networcat.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'bajczi-molnr-networcatapplyinganalysistechniquesofsharedmemorysoftwareonmessagepassingdistributedsystems-2025', 'https://leventebajczi.github.io/publications/sosym25networcat.pdf', event);\">\n    NetworCat: applying analysis techniques of shared memory software on message-passing distributed systems.\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>;  and Molnár, V.\n</span>\n\n  \n\n</span>\n\n  <i>SOFTWARE AND SYSTEMS MODELING</i>.  2025.\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/sosym25networcat.pdf\"\n     onclick=\"log_download('bajczi-molnr-networcatapplyinganalysistechniquesofsharedmemorysoftwareonmessagepassingdistributedsystems-2025', 'https://leventebajczi.github.io/publications/sosym25networcat.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"NetworCat: applying analysis techniques of shared memory software on message-passing distributed systems [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://m2.mtmt.hu/api/publication/35762171\"\n     onclick=\"log_download('bajczi-molnr-networcatapplyinganalysistechniquesofsharedmemorysoftwareonmessagepassingdistributedsystems-2025', 'https://m2.mtmt.hu/api/publication/35762171', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"NetworCat: applying analysis techniques of shared memory software on message-passing distributed systems [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/s10270-024-01258-x\"\n     onclick=\"log_download('bajczi-molnr-networcatapplyinganalysistechniquesofsharedmemorysoftwareonmessagepassingdistributedsystems-2025', 'http://doi.org/10.1007/s10270-024-01258-x', 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-molnr-networcatapplyinganalysistechniquesofsharedmemorysoftwareonmessagepassingdistributedsystems-2025\"\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-molnr-networcatapplyinganalysistechniquesofsharedmemorysoftwareonmessagepassingdistributedsystems-2025')\" -->\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:35762171,\n\ttitle = {{NetworCat: applying analysis techniques of shared memory software on message-passing distributed systems}},\n\tauthor = {Bajczi, Levente and Molnár, Vince},\n\tdoi = {10.1007/s10270-024-01258-x},\n\tjournal-iso = {SOFTW SYST MODEL},\n\tjournal = {SOFTWARE AND SYSTEMS MODELING},\n\tunique-id = {35762171},\n\tissn = {1619-1366},\n\tabstract = {Communication models are a key aspect in the design and implementation of distributed system architectures. Application logic must consider the guarantees of these models, which fundamentally influence its correctness. Modern multi-core processor architectures face a similar problem when it comes to accessing shared memory: the guarantees of an architecture have a fundamental impact on the observable behavior of software. The formalization of these guarantees in a declarative way has led to powerful tools and algorithms to define reusable constraints on patterns of memory access events and their relationships, enabling the efficient description and automatic formal analysis of software properties with respect to a specific architecture. The Cat memory modeling language provides a standard means of specifying these constraints. Despite the parallels, the axiomatic modeling and analysis of communication models in distributed systems remain a relatively unexplored area. In this paper, we address this gap and demonstrate how communication models can be mapped to the Cat language. We create a standard library of reusable patterns and demonstrate our approach, called NetworCat , on the simple examples of UDP and TCP, and we also present its applicability to the vastly configurable OMG-DDS service. This adaptation-based approach enables the use of ever-improving verification tools built for shared memory concurrency on distributed systems. We believe this not only benefits distributed system analyses by broadening the toolset for verification but also positively impacts the field of memory-model-aware verification by widening its audience to another domain.},\n\tyear = {2025},\n\teissn = {1619-1374},\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/sosym25networcat.pdf},\n\turl_mtmt   = {https://m2.mtmt.hu/api/publication/35762171},\n}\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  Communication models are a key aspect in the design and implementation of distributed system architectures. Application logic must consider the guarantees of these models, which fundamentally influence its correctness. Modern multi-core processor architectures face a similar problem when it comes to accessing shared memory: the guarantees of an architecture have a fundamental impact on the observable behavior of software. The formalization of these guarantees in a declarative way has led to powerful tools and algorithms to define reusable constraints on patterns of memory access events and their relationships, enabling the efficient description and automatic formal analysis of software properties with respect to a specific architecture. The Cat memory modeling language provides a standard means of specifying these constraints. Despite the parallels, the axiomatic modeling and analysis of communication models in distributed systems remain a relatively unexplored area. In this paper, we address this gap and demonstrate how communication models can be mapped to the Cat language. We create a standard library of reusable patterns and demonstrate our approach, called NetworCat , on the simple examples of UDP and TCP, and we also present its applicability to the vastly configurable OMG-DDS service. This adaptation-based approach enables the use of ever-improving verification tools built for shared memory concurrency on distributed systems. We believe this not only benefits distributed system analyses by broadening the toolset for verification but also positively impacts the field of memory-model-aware verification by widening its audience to another domain.\n</div>\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"telbisz-bajczi-szekeres-vrs-thetavariousapproachesforconcurrentprogramverificationcompetitioncontribution-2025\">\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/tacas25theta.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'telbisz-bajczi-szekeres-vrs-thetavariousapproachesforconcurrentprogramverificationcompetitioncontribution-2025', 'https://leventebajczi.github.io/publications/tacas25theta.pdf', event);\">\n    Theta: Various Approaches for Concurrent Program Verification (Competition Contribution).\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  Telbisz, C. F.; <a class=\"bibbase author link\" href=\"https://leventebajczi.com/publications.html\">Bajczi, L.</a>; Szekeres, D.;  and Vörös, A.\n</span>\n\n  \n\n</span>\n\n  <i>LECTURE NOTES IN COMPUTER SCIENCE</i>, 15698: 260-265.  2025.\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/tacas25theta.pdf\"\n     onclick=\"log_download('telbisz-bajczi-szekeres-vrs-thetavariousapproachesforconcurrentprogramverificationcompetitioncontribution-2025', 'https://leventebajczi.github.io/publications/tacas25theta.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"Theta: Various Approaches for Concurrent Program Verification (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/posters/tacas25.pdf\"\n     onclick=\"log_download('telbisz-bajczi-szekeres-vrs-thetavariousapproachesforconcurrentprogramverificationcompetitioncontribution-2025', 'https://leventebajczi.github.io/publications/posters/tacas25.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"Theta: Various Approaches for Concurrent Program Verification (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/36122885\"\n     onclick=\"log_download('telbisz-bajczi-szekeres-vrs-thetavariousapproachesforconcurrentprogramverificationcompetitioncontribution-2025', 'https://m2.mtmt.hu/api/publication/36122885', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"Theta: Various Approaches for Concurrent Program Verification (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-90660-2_22\"\n     onclick=\"log_download('telbisz-bajczi-szekeres-vrs-thetavariousapproachesforconcurrentprogramverificationcompetitioncontribution-2025', 'http://doi.org/10.1007/978-3-031-90660-2_22', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/telbisz-bajczi-szekeres-vrs-thetavariousapproachesforconcurrentprogramverificationcompetitioncontribution-2025\"\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('telbisz-bajczi-szekeres-vrs-thetavariousapproachesforconcurrentprogramverificationcompetitioncontribution-2025')\" -->\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:36122885,\n\ttitle = {Theta: Various Approaches for Concurrent Program Verification (Competition Contribution)},\n\tauthor = {Telbisz, Csanád Ferenc and Bajczi, Levente and Szekeres, Dániel and Vörös, András},\n\tdoi = {10.1007/978-3-031-90660-2_22},\n\tjournal-iso = {LNCS},\n\tjournal = {LECTURE NOTES IN COMPUTER SCIENCE},\n\tvolume = {15698},\n\tunique-id = {36122885},\n\tissn = {0302-9743},\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 2025, we complement our existing approach (abstraction-aware partial order reduction) for multi-threaded programs with a happens before propagator-based BMC check, expecting a significant increase in performance. We again utilize our portfolio with dynamic algorithm selection from last year, with improvements regarding solver choice and configuration ordering. In this paper, we detail our algorithmic improvements in Theta regarding the verification of concurrent software.},\n\tyear = {2025},\n\teissn = {1611-3349},\n\tpages = {260-265},\n\torcid-numbers = {Telbisz, Csanád Ferenc/0000-0002-6260-5908; Bajczi, Levente/0000-0002-6551-5860; Szekeres, Dániel/0000-0002-2912-028X},\n\n\n    url_pdf    = {https://leventebajczi.github.io/publications/tacas25theta.pdf},\n\turl_poster = {https://leventebajczi.github.io/publications/posters/tacas25.pdf},\n\turl_mtmt   = {https://m2.mtmt.hu/api/publication/36122885},\t\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 2025, we complement our existing approach (abstraction-aware partial order reduction) for multi-threaded programs with a happens before propagator-based BMC check, expecting a significant increase in performance. We again utilize our portfolio with dynamic algorithm selection from last year, with improvements regarding solver choice and configuration ordering. In this paper, we detail our algorithmic improvements in Theta regarding the verification of concurrent software.\n</div>\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"bajczi-dm-micskei-svcomp25reproductionreportcompetitioncontribution-2025\">\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/tacas25repro.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'bajczi-dm-micskei-svcomp25reproductionreportcompetitioncontribution-2025', 'https://leventebajczi.github.io/publications/tacas25repro.pdf', event);\">\n    SV-COMP’25 Reproduction Report (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  <i>LECTURE NOTES IN COMPUTER SCIENCE</i>, 15698: 187-191.  2025.\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/tacas25repro.pdf\"\n     onclick=\"log_download('bajczi-dm-micskei-svcomp25reproductionreportcompetitioncontribution-2025', 'https://leventebajczi.github.io/publications/tacas25repro.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"SV-COMP’25 Reproduction Report (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/tacas25repro.pdf\"\n     onclick=\"log_download('bajczi-dm-micskei-svcomp25reproductionreportcompetitioncontribution-2025', 'https://leventebajczi.github.io/publications/slides/tacas25repro.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"SV-COMP’25 Reproduction Report (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/36122888\"\n     onclick=\"log_download('bajczi-dm-micskei-svcomp25reproductionreportcompetitioncontribution-2025', 'https://m2.mtmt.hu/api/publication/36122888', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"SV-COMP’25 Reproduction Report (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-90660-2_10\"\n     onclick=\"log_download('bajczi-dm-micskei-svcomp25reproductionreportcompetitioncontribution-2025', 'http://doi.org/10.1007/978-3-031-90660-2_10', 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-svcomp25reproductionreportcompetitioncontribution-2025\"\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-dm-micskei-svcomp25reproductionreportcompetitioncontribution-2025')\" -->\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:36122888,\n\ttitle = {SV-COMP’25 Reproduction Report (Competition Contribution)},\n\tauthor = {Bajczi, Levente and Ádám, Zsófia and Micskei, Zoltán Imre},\n\tdoi = {10.1007/978-3-031-90660-2_10},\n\tjournal-iso = {LNCS},\n\tjournal = {LECTURE NOTES IN COMPUTER SCIENCE},\n\tvolume = {15698},\n\tunique-id = {36122888},\n\tissn = {0302-9743},\n\tabstract = {The International Competition on Software Verification (SV-COMP) has been an important driver of progress in the formal verification community, fostering tool development, benchmarking, and reproducibility. As the competition grows in scale and complexity, a reproducibility study is essential to evaluate its robustness across environments, uncover hidden dependencies, and ensure long-term sustainability. This work aims to reaffirm the reliability of SV-COMP’s results, provide insights for similar competitions, and facilitate the adoption of its infrastructure beyond the competition. We reproduced the verification and validation results of active participants, including score and ranking calculations for the verification track. We found several problems prohibiting reusability and reproducibility of some participating tools, but we did not find serious issues with the competition infrastructure itself.},\n\tyear = {2025},\n\teissn = {1611-3349},\n\tpages = {187-191},\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\n    url_pdf    = {https://leventebajczi.github.io/publications/tacas25repro.pdf},\n\turl_slides = {https://leventebajczi.github.io/publications/slides/tacas25repro.pdf},\n\turl_mtmt   = {https://m2.mtmt.hu/api/publication/36122888},\t\n}\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  The International Competition on Software Verification (SV-COMP) has been an important driver of progress in the formal verification community, fostering tool development, benchmarking, and reproducibility. As the competition grows in scale and complexity, a reproducibility study is essential to evaluate its robustness across environments, uncover hidden dependencies, and ensure long-term sustainability. This work aims to reaffirm the reliability of SV-COMP’s results, provide insights for similar competitions, and facilitate the adoption of its infrastructure beyond the competition. We reproduced the verification and validation results of active participants, including score and ranking calculations for the verification track. We found several problems prohibiting reusability and reproducibility of some participating tools, but we did not find serious issues with the competition infrastructure itself.\n</div>\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"mondok-bajczi-szekeres-molnr-emergenthetavariationsonsymbolictransitionsystemscompetitioncontribution-2025\">\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/tacas25etheta.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'mondok-bajczi-szekeres-molnr-emergenthetavariationsonsymbolictransitionsystemscompetitioncontribution-2025', 'https://leventebajczi.github.io/publications/tacas25etheta.pdf', event);\">\n    EmergenTheta: Variations on Symbolic Transition Systems (Competition Contribution).\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  Mondok, M.; <a class=\"bibbase author link\" href=\"https://leventebajczi.com/publications.html\">Bajczi, L.</a>; Szekeres, D.;  and Molnár, V.\n</span>\n\n  \n\n</span>\n\n  <i>LECTURE NOTES IN COMPUTER SCIENCE</i>, 15698: 217-222.  2025.\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/tacas25etheta.pdf\"\n     onclick=\"log_download('mondok-bajczi-szekeres-molnr-emergenthetavariationsonsymbolictransitionsystemscompetitioncontribution-2025', 'https://leventebajczi.github.io/publications/tacas25etheta.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"EmergenTheta: Variations on Symbolic Transition Systems (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/tacas25etheta.pdf\"\n     onclick=\"log_download('mondok-bajczi-szekeres-molnr-emergenthetavariationsonsymbolictransitionsystemscompetitioncontribution-2025', 'https://leventebajczi.github.io/publications/slides/tacas25etheta.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"EmergenTheta: Variations on Symbolic Transition Systems (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/36122891\"\n     onclick=\"log_download('mondok-bajczi-szekeres-molnr-emergenthetavariationsonsymbolictransitionsystemscompetitioncontribution-2025', 'https://m2.mtmt.hu/api/publication/36122891', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"EmergenTheta: Variations on Symbolic Transition Systems (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-90660-2_15\"\n     onclick=\"log_download('mondok-bajczi-szekeres-molnr-emergenthetavariationsonsymbolictransitionsystemscompetitioncontribution-2025', 'http://doi.org/10.1007/978-3-031-90660-2_15', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/mondok-bajczi-szekeres-molnr-emergenthetavariationsonsymbolictransitionsystemscompetitioncontribution-2025\"\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('mondok-bajczi-szekeres-molnr-emergenthetavariationsonsymbolictransitionsystemscompetitioncontribution-2025')\" -->\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:36122891,\n\ttitle = {{EmergenTheta: Variations on Symbolic Transition Systems (Competition Contribution)}},\n\tauthor = {Mondok, Milán and Bajczi, Levente and Szekeres, Dániel and Molnár, Vince},\n\tdoi = {10.1007/978-3-031-90660-2_15},\n\tjournal-iso = {LNCS},\n\tjournal = {LECTURE NOTES IN COMPUTER SCIENCE},\n\tvolume = {15698},\n\tunique-id = {36122891},\n\tissn = {0302-9743},\n\tabstract = {EmergenTheta is our sandbox for experimental analyses. After its successful debut in SV-COMP’24, we kept some well-performing but still under-tested configurations, and complemented them with a new saturation algorithm over decision diagrams, and two ways of extending their verification power: wrapping them in a lightweight, counterexample-guided abstraction refinement (CEGAR) loop based on implicit predicate abstraction; and backwards traversal of the state space. All such analyses now rely on a common interface to the underlying symbolic transition system, integrating seamlessly into the existing Theta framework. Using this combination of proven analyses and novel extensions, EmergenTheta outperformed our expectations in SV-COMP’25.},\n\tyear = {2025},\n\teissn = {1611-3349},\n\tpages = {217-222},\n\torcid-numbers = {Mondok, Milán/0000-0001-5396-2172; Bajczi, Levente/0000-0002-6551-5860; Szekeres, Dániel/0000-0002-2912-028X; Molnár, Vince/0000-0002-8204-7595},\n\n    url_pdf    = {https://leventebajczi.github.io/publications/tacas25etheta.pdf},\n\turl_slides = {https://leventebajczi.github.io/publications/slides/tacas25etheta.pdf},\n\turl_mtmt   = {https://m2.mtmt.hu/api/publication/36122891},\t\n}\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  EmergenTheta is our sandbox for experimental analyses. After its successful debut in SV-COMP’24, we kept some well-performing but still under-tested configurations, and complemented them with a new saturation algorithm over decision diagrams, and two ways of extending their verification power: wrapping them in a lightweight, counterexample-guided abstraction refinement (CEGAR) loop based on implicit predicate abstraction; and backwards traversal of the state space. All such analyses now rely on a common interface to the underlying symbolic transition system, integrating seamlessly into the existing Theta framework. Using this combination of proven analyses and novel extensions, EmergenTheta outperformed our expectations in SV-COMP’25.\n</div>\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"bajczi-telbisz-szekeres-vrs-onstabilityinahappensbeforepropagatorforconcurrentprogramsreproducibilitystudy-2025\">\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/tacas25ocfix.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'bajczi-telbisz-szekeres-vrs-onstabilityinahappensbeforepropagatorforconcurrentprogramsreproducibilitystudy-2025', 'https://leventebajczi.github.io/publications/tacas25ocfix.pdf', event);\">\n    On Stability in a Happens-Before Propagator for Concurrent Programs (Reproducibility Study).\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. F.; Szekeres, D.;  and Vörös, A.\n</span>\n\n  \n\n</span>\n\n  <i>LECTURE NOTES IN COMPUTER SCIENCE</i>, 15696: 3-19.  2025.\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/tacas25ocfix.pdf\"\n     onclick=\"log_download('bajczi-telbisz-szekeres-vrs-onstabilityinahappensbeforepropagatorforconcurrentprogramsreproducibilitystudy-2025', 'https://leventebajczi.github.io/publications/tacas25ocfix.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"On Stability in a Happens-Before Propagator for Concurrent Programs (Reproducibility Study) [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/tacas25ocfix.pdf\"\n     onclick=\"log_download('bajczi-telbisz-szekeres-vrs-onstabilityinahappensbeforepropagatorforconcurrentprogramsreproducibilitystudy-2025', 'https://leventebajczi.github.io/publications/slides/tacas25ocfix.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"On Stability in a Happens-Before Propagator for Concurrent Programs (Reproducibility Study) [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/36122897\"\n     onclick=\"log_download('bajczi-telbisz-szekeres-vrs-onstabilityinahappensbeforepropagatorforconcurrentprogramsreproducibilitystudy-2025', 'https://m2.mtmt.hu/api/publication/36122897', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"On Stability in a Happens-Before Propagator for Concurrent Programs (Reproducibility Study) [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-90643-5_1\"\n     onclick=\"log_download('bajczi-telbisz-szekeres-vrs-onstabilityinahappensbeforepropagatorforconcurrentprogramsreproducibilitystudy-2025', 'http://doi.org/10.1007/978-3-031-90643-5_1', 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-szekeres-vrs-onstabilityinahappensbeforepropagatorforconcurrentprogramsreproducibilitystudy-2025\"\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-telbisz-szekeres-vrs-onstabilityinahappensbeforepropagatorforconcurrentprogramsreproducibilitystudy-2025')\" -->\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:36122897,\n\ttitle = {On Stability in a Happens-Before Propagator for Concurrent Programs (Reproducibility Study)},\n\tauthor = {Bajczi, Levente and Telbisz, Csanád Ferenc and Szekeres, Dániel and Vörös, András},\n\tdoi = {10.1007/978-3-031-90643-5_1},\n\tjournal-iso = {LNCS},\n\tjournal = {LECTURE NOTES IN COMPUTER SCIENCE},\n\tvolume = {15696},\n\tunique-id = {36122897},\n\tissn = {0302-9743},\n\tabstract = {Analyzing concurrent programs often involves reasoning about happens-before relations, handled by dedicated SMT theory solvers. Recently, preventative propagation rules have been introduced for consistency models to avoid unnecessary computations. This paper analyses the reproducibility of a recently published paper regarding a conflict-avoiding happens-before propagator. We show that the underlying axioms are insufficient for supporting sequential consistency. We find that the algorithm can leave out constraints on event ordering (even considering the original axioms), impacting the accuracy of verification. We show a simple counterexample to the stability claim in the paper. Two revisions of the algorithm are presented, and a proof on the correctness of these approaches respective of the original axioms is shown. The tool implementing the original algorithm is examined to ascertain how it circumvents wrong results. It is found that it deviates from the published algorithm. We show that an unmodified algorithm (via a patch in the implementing tool) causes incorrect results. We also show that our revised algorithm can be implemented efficiently in an independent verification tool.},\n\tyear = {2025},\n\teissn = {1611-3349},\n\tpages = {3-19},\n\torcid-numbers = {Bajczi, Levente/0000-0002-6551-5860; Telbisz, Csanád Ferenc/0000-0002-6260-5908; Szekeres, Dániel/0000-0002-2912-028X},\n\n    url_pdf    = {https://leventebajczi.github.io/publications/tacas25ocfix.pdf},\n\turl_slides = {https://leventebajczi.github.io/publications/slides/tacas25ocfix.pdf},\n\turl_mtmt   = {https://m2.mtmt.hu/api/publication/36122897},\t\n}</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  Analyzing concurrent programs often involves reasoning about happens-before relations, handled by dedicated SMT theory solvers. Recently, preventative propagation rules have been introduced for consistency models to avoid unnecessary computations. This paper analyses the reproducibility of a recently published paper regarding a conflict-avoiding happens-before propagator. We show that the underlying axioms are insufficient for supporting sequential consistency. We find that the algorithm can leave out constraints on event ordering (even considering the original axioms), impacting the accuracy of verification. We show a simple counterexample to the stability claim in the paper. Two revisions of the algorithm are presented, and a proof on the correctness of these approaches respective of the original axioms is shown. The tool implementing the original algorithm is examined to ascertain how it circumvents wrong results. It is found that it deviates from the published algorithm. We show that an unmodified algorithm (via a patch in the implementing tool) causes incorrect results. We also show that our revised algorithm can be implemented efficiently in an independent verification tool.\n</div>\n\n\n</div>\n\n\n\n\n\n    </div>\n  </div>\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        (7)\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>4 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>5 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>2 downloads</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\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  <div class=\"bibbase_paper\" id=\"bajczi-szekeres-siegl-molnr-verbesserungdermbseausbildungdurchversionskontrolleundautomatisiertesfeedback-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/tdse24verbesserung.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'bajczi-szekeres-siegl-molnr-verbesserungdermbseausbildungdurchversionskontrolleundautomatisiertesfeedback-2024', 'https://leventebajczi.github.io/publications/tdse24verbesserung.pdf', event);\">\n    Verbesserung der MBSE-Ausbildung durch Versionskontrolle und automatisiertes Feedback.\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.; Siegl, D.;  and Molnár, V.\n</span>\n\n  \n\n</span>\n\n  In <i>Tag des Systems Engineering</i>, pages 161-169,  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/tdse24verbesserung.pdf\"\n     onclick=\"log_download('bajczi-szekeres-siegl-molnr-verbesserungdermbseausbildungdurchversionskontrolleundautomatisiertesfeedback-2024', 'https://leventebajczi.github.io/publications/tdse24verbesserung.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"Verbesserung der MBSE-Ausbildung durch Versionskontrolle und automatisiertes Feedback [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/tdse24verbesserung.pdf\"\n     onclick=\"log_download('bajczi-szekeres-siegl-molnr-verbesserungdermbseausbildungdurchversionskontrolleundautomatisiertesfeedback-2024', 'https://leventebajczi.github.io/publications/slides/tdse24verbesserung.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"Verbesserung der MBSE-Ausbildung durch Versionskontrolle und automatisiertes Feedback [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/35617761\"\n     onclick=\"log_download('bajczi-szekeres-siegl-molnr-verbesserungdermbseausbildungdurchversionskontrolleundautomatisiertesfeedback-2024', 'https://m2.mtmt.hu/api/publication/35617761', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"Verbesserung der MBSE-Ausbildung durch Versionskontrolle und automatisiertes Feedback [link]\"\n       title=\" mtmt\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\"> mtmt</span></a>\n  &nbsp;\n  \n\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/bajczi-szekeres-siegl-molnr-verbesserungdermbseausbildungdurchversionskontrolleundautomatisiertesfeedback-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\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-siegl-molnr-verbesserungdermbseausbildungdurchversionskontrolleundautomatisiertesfeedback-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:35617761,\n\ttitle = {Verbesserung der MBSE-Ausbildung durch Versionskontrolle und automatisiertes Feedback},\n\tauthor = {Bajczi, Levente and Szekeres, Dániel and Siegl, Daniel and Molnár, Vince},\n\tbooktitle = {Tag des Systems Engineering},\n\tunique-id = {35617761},\n\tyear = {2024},\n\tpages = {161-169},\n\torcid-numbers = {Bajczi, Levente/0000-0002-6551-5860; Szekeres, Dániel/0000-0002-2912-028X; Molnár, Vince/0000-0002-8204-7595},\n\n    url_pdf    = {https://leventebajczi.github.io/publications/tdse24verbesserung.pdf},\n    url_slides = {https://leventebajczi.github.io/publications/slides/tdse24verbesserung.pdf},\n    url_mtmt = {https://m2.mtmt.hu/api/publication/35617761},\n}\n\n</pre>\n</div>\n\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"bajczi-szekeres-siegl-molnr-enhancingmbseeducationwithversioncontrolandautomatedfeedback-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/tdse24enhancing.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'bajczi-szekeres-siegl-molnr-enhancingmbseeducationwithversioncontrolandautomatedfeedback-2024', 'https://leventebajczi.github.io/publications/tdse24enhancing.pdf', event);\">\n    Enhancing MBSE Education with Version Control and Automated Feedback.\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.; Siegl, D.;  and Molnár, V.\n</span>\n\n  \n\n</span>\n\n   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/tdse24enhancing.pdf\"\n     onclick=\"log_download('bajczi-szekeres-siegl-molnr-enhancingmbseeducationwithversioncontrolandautomatedfeedback-2024', 'https://leventebajczi.github.io/publications/tdse24enhancing.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"Enhancing MBSE Education with Version Control and Automated Feedback [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/tdse24verbesserung.pdf\"\n     onclick=\"log_download('bajczi-szekeres-siegl-molnr-enhancingmbseeducationwithversioncontrolandautomatedfeedback-2024', 'https://leventebajczi.github.io/publications/slides/tdse24verbesserung.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"Enhancing MBSE Education with Version Control and Automated Feedback [pdf]\"\n       title=\" slides\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\"> slides</span></a>\n  &nbsp;\n  \n\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/bajczi-szekeres-siegl-molnr-enhancingmbseeducationwithversioncontrolandautomatedfeedback-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\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('bajczi-szekeres-siegl-molnr-enhancingmbseeducationwithversioncontrolandautomatedfeedback-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;\">@misc{bajczi2024enhancingmbseeducationversion,\n\ttitle={Enhancing MBSE Education with Version Control and Automated Feedback}, \n\tauthor={Levente Bajczi and Dániel Szekeres and Daniel Siegl and Vince Molnár},\n\tyear={2024},\n\teprint={2409.15294},\n\tarchivePrefix={arXiv},\n\tprimaryClass={cs.CY},\n\n\turl_pdf    = {https://leventebajczi.github.io/publications/tdse24enhancing.pdf},\n    url_slides = {https://leventebajczi.github.io/publications/slides/tdse24verbesserung.pdf},\n}\n\n\n</pre>\n</div>\n\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"somorjai-doboskovcs-dm-bajczi-vrs-bottomsupforchcsnoveltransformationoflinearconstrainedhornclausestosoftwareverification-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/hcvs24chc.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'somorjai-doboskovcs-dm-bajczi-vrs-bottomsupforchcsnoveltransformationoflinearconstrainedhornclausestosoftwareverification-2024', 'https://leventebajczi.github.io/publications/hcvs24chc.pdf', event);\">\n    Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  Somorjai, M.; Dobos-Kovács, M.; Ádám, Z.; <a class=\"bibbase author link\" href=\"https://leventebajczi.com/publications.html\">Bajczi, L.</a>;  and Vörös, A.\n</span>\n\n  \n\n</span>\n\n  <i>ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE</i>, 402: 105-117.  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/hcvs24chc.pdf\"\n     onclick=\"log_download('somorjai-doboskovcs-dm-bajczi-vrs-bottomsupforchcsnoveltransformationoflinearconstrainedhornclausestosoftwareverification-2024', 'https://leventebajczi.github.io/publications/hcvs24chc.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software 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://m2.mtmt.hu/api/publication/33784283\"\n     onclick=\"log_download('somorjai-doboskovcs-dm-bajczi-vrs-bottomsupforchcsnoveltransformationoflinearconstrainedhornclausestosoftwareverification-2024', 'https://m2.mtmt.hu/api/publication/33784283', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software 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.4204/EPTCS.402.11\"\n     onclick=\"log_download('somorjai-doboskovcs-dm-bajczi-vrs-bottomsupforchcsnoveltransformationoflinearconstrainedhornclausestosoftwareverification-2024', 'http://doi.org/10.4204/EPTCS.402.11', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/somorjai-doboskovcs-dm-bajczi-vrs-bottomsupforchcsnoveltransformationoflinearconstrainedhornclausestosoftwareverification-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\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('somorjai-doboskovcs-dm-bajczi-vrs-bottomsupforchcsnoveltransformationoflinearconstrainedhornclausestosoftwareverification-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;\">@article{MTMT:33784283,\n\ttitle = {Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification},\n\tauthor = {Somorjai, Márk and Dobos-Kovács, Mihály and Ádám, Zsófia and Bajczi, Levente and Vörös, András},\n\tdoi = {10.4204/EPTCS.402.11},\n\tjournal-iso = {ELECTRON PROC THEOR COMPUT SCI},\n\tjournal = {ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE},\n\tvolume = {402},\n\tunique-id = {33784283},\n\tabstract = {Constrained Horn Clauses (CHCs) have conventionally been used as a low-level representation in formal verification. Most existing solvers use a diverse set of specialized techniques, including direct state space traversal or under-approximating abstraction, necessitating purpose-built complex algorithms. Other solvers successfully simplified the verification workflow by translating the problem to inputs for other verification tasks, leveraging the strengths of existing algorithms. One such approach transforms the CHC problem into a recursive program roughly emulating a top-down solver for the deduction task; and verifying the reachability of a safety violation specified as a control location. We propose an alternative bottom-up approach for linear CHCs, and evaluate the two options in the open-source model checking framework THETA on both synthetic and industrial examples. We find that there is a more than twofold increase in the number of solved tasks when the novel bottom-up approach is used in the verification workflow, in contrast with the top-down technique. © Márk Somorjai et al.},\n\tyear = {2024},\n\teissn = {2075-2180},\n\tpages = {105-117},\n\torcid-numbers = {Dobos-Kovács, Mihály/0000-0002-0064-2965; Ádám, Zsófia/0000-0003-2354-1750; Bajczi, Levente/0000-0002-6551-5860},\n\n    url_pdf    = {https://leventebajczi.github.io/publications/hcvs24chc.pdf},\n\turl_mtmt   = {https://m2.mtmt.hu/api/publication/33784283},\t\n}\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  Constrained Horn Clauses (CHCs) have conventionally been used as a low-level representation in formal verification. Most existing solvers use a diverse set of specialized techniques, including direct state space traversal or under-approximating abstraction, necessitating purpose-built complex algorithms. Other solvers successfully simplified the verification workflow by translating the problem to inputs for other verification tasks, leveraging the strengths of existing algorithms. One such approach transforms the CHC problem into a recursive program roughly emulating a top-down solver for the deduction task; and verifying the reachability of a safety violation specified as a control location. We propose an alternative bottom-up approach for linear CHCs, and evaluate the two options in the open-source model checking framework THETA on both synthetic and industrial examples. We find that there is a more than twofold increase in the number of solved tasks when the novel bottom-up approach is used in the verification workflow, in contrast with the top-down technique. © Márk Somorjai et al.\n</div>\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"bajczi-molnr-solvingconstrainedhornclausesascprogramswithchc2c-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/spin24chc2c.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'bajczi-molnr-solvingconstrainedhornclausesascprogramswithchc2c-2024', 'https://leventebajczi.github.io/publications/spin24chc2c.pdf', event);\">\n    Solving Constrained Horn Clauses as C Programs with CHC2C.\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>;  and Molnár, V.\n</span>\n\n  \n\n</span>\n\n  <i>LECTURE NOTES IN COMPUTER SCIENCE</i>, 14624: 146-163.  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/spin24chc2c.pdf\"\n     onclick=\"log_download('bajczi-molnr-solvingconstrainedhornclausesascprogramswithchc2c-2024', 'https://leventebajczi.github.io/publications/spin24chc2c.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"Solving Constrained Horn Clauses as C Programs with CHC2C [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/spin24chc2c.pdf\"\n     onclick=\"log_download('bajczi-molnr-solvingconstrainedhornclausesascprogramswithchc2c-2024', 'https://leventebajczi.github.io/publications/slides/spin24chc2c.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"Solving Constrained Horn Clauses as C Programs with CHC2C [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/34853031\"\n     onclick=\"log_download('bajczi-molnr-solvingconstrainedhornclausesascprogramswithchc2c-2024', 'https://m2.mtmt.hu/api/publication/34853031', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"Solving Constrained Horn Clauses as C Programs with CHC2C [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-66149-5_8\"\n     onclick=\"log_download('bajczi-molnr-solvingconstrainedhornclausesascprogramswithchc2c-2024', 'http://doi.org/10.1007/978-3-031-66149-5_8', 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-molnr-solvingconstrainedhornclausesascprogramswithchc2c-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\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('bajczi-molnr-solvingconstrainedhornclausesascprogramswithchc2c-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  \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:34853031,\n\ttitle = {Solving Constrained Horn Clauses as C Programs with CHC2C},\n\tauthor = {Bajczi, Levente and Molnár, Vince},\n\tdoi = {10.1007/978-3-031-66149-5_8},\n\tjournal-iso = {LNCS},\n\tjournal = {LECTURE NOTES IN COMPUTER SCIENCE},\n\tvolume = {14624},\n\tunique-id = {34853031},\n\tissn = {0302-9743},\n\tabstract = {Solving Constrained Horn Clauses (CHC) is necessitated by numerous fields in formal methods, from verifying software and smart contracts to modeling systems, yet the competitive scene for academic tools remains fairly sparse, especially compared to more popular fields such as software verification. Comparative evaluation as a competition, such as SV-COMP or CHC-COMP, sparks a more cohesive community around fields in formal methods. Lately, a trend has been emerging with tools such as Btor2C that bridge multiple fields together, thus widening this cohesion. Following that example, we propose and perform an experiment, where we use CHC-to-C transformation to apply software verification tools to linear CHC problems. In the process, we help both fields by diversifying the scene of CHC solvers and providing new and valuable benchmarks to aid the development of software verification tools. Using these benchmarks, we uncovered a previously hidden bug in multiple verification tools that can lead to false positive results. By analysing the results of the experiment, we can confidently make a recommendation for developers of software verifiers to consider supporting CHCs via our pre-verification transformation.},\n\tkeywords = {verification; formal methods; Computer Science, Software Engineering; CHC},\n\tyear = {2024},\n\teissn = {1611-3349},\n\tpages = {146-163},\n\torcid-numbers = {Bajczi, Levente/0000-0002-6551-5860; Molnár, Vince/0000-0002-8204-7595},\n\n\n    url_pdf    = {https://leventebajczi.github.io/publications/spin24chc2c.pdf},\n    url_slides = {https://leventebajczi.github.io/publications/slides/spin24chc2c.pdf},\n\turl_mtmt   = {https://m2.mtmt.hu/api/publication/34853031},\t\n}\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  Solving Constrained Horn Clauses (CHC) is necessitated by numerous fields in formal methods, from verifying software and smart contracts to modeling systems, yet the competitive scene for academic tools remains fairly sparse, especially compared to more popular fields such as software verification. Comparative evaluation as a competition, such as SV-COMP or CHC-COMP, sparks a more cohesive community around fields in formal methods. Lately, a trend has been emerging with tools such as Btor2C that bridge multiple fields together, thus widening this cohesion. Following that example, we propose and perform an experiment, where we use CHC-to-C transformation to apply software verification tools to linear CHC problems. In the process, we help both fields by diversifying the scene of CHC solvers and providing new and valuable benchmarks to aid the development of software verification tools. Using these benchmarks, we uncovered a previously hidden bug in multiple verification tools that can lead to false positive results. By analysing the results of the experiment, we can confidently make a recommendation for developers of software verifiers to consider supporting CHCs via our pre-verification transformation.\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>6 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  &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-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);