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://csanadtelbisz.github.io/publications.bib\",\"jsonp\":\"1\",\"theme\":\"side\",\"host\":\"bibbase.org\",\"ssl\":false},\n      data: [{\"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://csanadtelbisz.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\\t\\n\\turl_pdf = {https://csanadtelbisz.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},\\n}\\n\\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://csanadtelbisz.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\":\"\",\"downloads\":1},{\"bibtype\":\"inproceedings\",\"type\":\"inproceedings\",\"title\":\"Giving Some Pointers for Abstraction-Based Model Checking\",\"author\":[{\"propositions\":[],\"lastnames\":[\"Bajczi\"],\"firstnames\":[\"Levente\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Szekeres\"],\"firstnames\":[\"Dániel\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Telbisz\"],\"firstnames\":[\"Csanád\",\"Ferenc\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Molnár\"],\"firstnames\":[\"Vince\"],\"suffixes\":[]}],\"booktitle\":\"Proceedings of the 32nd Minisymposium\",\"doi\":\"10.3311/MINISY2025-002\",\"unique-id\":\"36176199\",\"abstract\":\"Abstraction-based software model checkers often rely on external analyses or unbounded SMT arrays to reason about pointers, arrays, and dynamic heap manipulation. External analyses are precise but often require the modification of existing verification algorithms, while SMT arrays provide a native solution for solver-based verifiers but require strict type safety often forgone in real-world programs. We propose a novel way of integrating a precise pointer and array analysis as a plug-in for abstraction-based model checking, which does not require the modification of the underlying algorithms. Our solution keeps track of arbitrary predicates over potentially abstract memory locations, moving toward more efficient verification of software code by allowing a fine-grained and precise abstraction of memory accesses.\",\"year\":\"2025\",\"pages\":\"5-9\",\"orcid-numbers\":\"Bajczi, Levente/0000-0002-6551-5860; Szekeres, Dániel/0000-0002-2912-028X; Telbisz, Csanád Ferenc/0000-0002-6260-5908; Molnár, Vince/0000-0002-8204-7595\",\"url_pdf\":\"https://csanadtelbisz.github.io/publications/minisy25pointers.pdf\",\"url_mtmt\":\"https://m2.mtmt.hu/api/publication/36176199\",\"bibtex\":\"@inproceedings{MTMT:36176199,\\n\\ttitle = {Giving Some Pointers for Abstraction-Based Model Checking},\\n\\tauthor = {Bajczi, Levente and Szekeres, Dániel and Telbisz, Csanád Ferenc and Molnár, Vince},\\n\\tbooktitle = {Proceedings of the 32nd Minisymposium},\\n\\tdoi = {10.3311/MINISY2025-002},\\n\\tunique-id = {36176199},\\n\\tabstract = {Abstraction-based software model checkers often rely on external analyses or unbounded SMT arrays to reason about pointers, arrays, and dynamic heap manipulation. External analyses are precise but often require the modification of existing verification algorithms, while SMT arrays provide a native solution for solver-based verifiers but require strict type safety often forgone in real-world programs. We propose a novel way of integrating a precise pointer and array analysis as a plug-in for abstraction-based model checking, which does not require the modification of the underlying algorithms. Our solution keeps track of arbitrary predicates over potentially abstract memory locations, moving toward more efficient verification of software code by allowing a fine-grained and precise abstraction of memory accesses.},\\n\\tyear = {2025},\\n\\tpages = {5-9},\\n\\torcid-numbers = {Bajczi, Levente/0000-0002-6551-5860; Szekeres, Dániel/0000-0002-2912-028X; Telbisz, Csanád Ferenc/0000-0002-6260-5908; Molnár, Vince/0000-0002-8204-7595},\\n\\t\\n\\turl_pdf = {https://csanadtelbisz.github.io/publications/minisy25pointers.pdf},\\n\\turl_mtmt = {https://m2.mtmt.hu/api/publication/36176199},\\n}\\n\\n\",\"author_short\":[\"Bajczi, L.\",\"Szekeres, D.\",\"Telbisz, C. F.\",\"Molnár, V.\"],\"key\":\"MTMT:36176199\",\"id\":\"MTMT:36176199\",\"bibbaseid\":\"bajczi-szekeres-telbisz-molnr-givingsomepointersforabstractionbasedmodelchecking-2025\",\"role\":\"author\",\"urls\":{\" pdf\":\"https://csanadtelbisz.github.io/publications/minisy25pointers.pdf\",\" mtmt\":\"https://m2.mtmt.hu/api/publication/36176199\"},\"metadata\":{\"authorlinks\":{\"bajczi, l\":\"https://leventebajczi.com/publications.html\"}},\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"inproceedings\",\"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://csanadtelbisz.github.io/publications/tacas25theta.pdf\",\"url_slides\":\"https://csanadtelbisz.github.io/publications/slides/tacas25theta.pdf\",\"url_mtmt\":\"https://m2.mtmt.hu/api/publication/36122885\",\"bibtex\":\"@inproceedings{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\\t\\n\\turl_pdf = {https://csanadtelbisz.github.io/publications/tacas25theta.pdf},\\n\\turl_slides = {https://csanadtelbisz.github.io/publications/slides/tacas25theta.pdf},\\n\\turl_mtmt = {https://m2.mtmt.hu/api/publication/36122885},\\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://csanadtelbisz.github.io/publications/tacas25theta.pdf\",\" slides\":\"https://csanadtelbisz.github.io/publications/slides/tacas25theta.pdf\",\" mtmt\":\"https://m2.mtmt.hu/api/publication/36122885\"},\"metadata\":{\"authorlinks\":{\"bajczi, l\":\"https://leventebajczi.com/publications.html\"}},\"downloads\":2,\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"inproceedings\",\"title\":\"Reasoning with Happens-Before Relations About Concurrent Programs in the THETA Framework\",\"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\":[]},{\"propositions\":[],\"lastnames\":[\"Majzik\"],\"firstnames\":[\"István\"],\"suffixes\":[]}],\"booktitle\":\"2025 55th Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshops (DSN-W)\",\"doi\":\"10.1109/DSN-W65791.2025.00037\",\"unique-id\":\"36267184\",\"abstract\":\"The model checking of multi-threaded programs often involves reasoning about the happens-before relation of concurrent program instructions. Several algorithms exist for finding a partial order of instructions that is consistent with ordering constraints of the assumed memory model and that violates a safety property; or for proving that such partial orders do not exist. We present existing and novel bounded model checking approaches reasoning with happens-before relations of concurrent programs. These algorithms are implemented in THETA, a modular model checking framework. We also give a comparative evaluation of our THETA implementations and state-of-the-art verifiers.\",\"year\":\"2025\",\"pages\":\"43-46\",\"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://csanadtelbisz.github.io/publications/verdi25oc.pdf\",\"url_mtmt\":\"https://m2.mtmt.hu/api/publication/36267184\",\"bibtex\":\"@inproceedings{MTMT:36267184,\\n\\ttitle = {Reasoning with Happens-Before Relations About Concurrent Programs in the THETA Framework},\\n\\tauthor = {Telbisz, Csanád Ferenc and Bajczi, Levente and Szekeres, Dániel and Vörös, András and Majzik, István},\\n\\tbooktitle = {2025 55th Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshops (DSN-W)},\\n\\tdoi = {10.1109/DSN-W65791.2025.00037},\\n\\tunique-id = {36267184},\\n\\tabstract = {The model checking of multi-threaded programs often involves reasoning about the happens-before relation of concurrent program instructions. Several algorithms exist for finding a partial order of instructions that is consistent with ordering constraints of the assumed memory model and that violates a safety property; or for proving that such partial orders do not exist. We present existing and novel bounded model checking approaches reasoning with happens-before relations of concurrent programs. These algorithms are implemented in THETA, a modular model checking framework. We also give a comparative evaluation of our THETA implementations and state-of-the-art verifiers.},\\n\\tyear = {2025},\\n\\tpages = {43-46},\\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\\t\\n\\turl_pdf = {https://csanadtelbisz.github.io/publications/verdi25oc.pdf},\\n\\turl_mtmt = {https://m2.mtmt.hu/api/publication/36267184},\\n}\\n\\n\",\"author_short\":[\"Telbisz, C. F.\",\"Bajczi, L.\",\"Szekeres, D.\",\"Vörös, A.\",\"Majzik, I.\"],\"key\":\"MTMT:36267184\",\"id\":\"MTMT:36267184\",\"bibbaseid\":\"telbisz-bajczi-szekeres-vrs-majzik-reasoningwithhappensbeforerelationsaboutconcurrentprogramsinthethetaframework-2025\",\"role\":\"author\",\"urls\":{\" pdf\":\"https://csanadtelbisz.github.io/publications/verdi25oc.pdf\",\" mtmt\":\"https://m2.mtmt.hu/api/publication/36267184\"},\"metadata\":{\"authorlinks\":{\"bajczi, l\":\"https://leventebajczi.com/publications.html\"}},\"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\",\"Ferenc\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Dobos-Kovács\"],\"firstnames\":[\"Mihály\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Molnár\"],\"firstnames\":[\"Vince\"],\"suffixes\":[]}],\"doi\":\"10.1007/978-3-031-57256-2_23\",\"journal-iso\":\"LNCS\",\"journal\":\"LECTURE NOTES IN COMPUTER SCIENCE\",\"volume\":\"14572\",\"unique-id\":\"34768422\",\"issn\":\"0302-9743\",\"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\",\"eissn\":\"1611-3349\",\"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 Ferenc/0000-0002-6260-5908; Dobos-Kovács, Mihály/0000-0002-0064-2965; Molnár, Vince/0000-0002-8204-7595\",\"url_pdf\":\"https://csanadtelbisz.github.io/publications/tacas24etheta.pdf\",\"url_slides\":\"https://leventebajczi.com/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 Ferenc and Dobos-Kovács, Mihály and Molnár, Vince},\\n\\tdoi = {10.1007/978-3-031-57256-2_23},\\n\\tjournal-iso = {LNCS},\\n\\tjournal = {LECTURE NOTES IN COMPUTER SCIENCE},\\n\\tvolume = {14572},\\n\\tunique-id = {34768422},\\n\\tissn = {0302-9743},\\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\\teissn = {1611-3349},\\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 Ferenc/0000-0002-6260-5908; Dobos-Kovács, Mihály/0000-0002-0064-2965; Molnár, Vince/0000-0002-8204-7595},\\n\\t\\n\\turl_pdf = {https://csanadtelbisz.github.io/publications/tacas24etheta.pdf},\\n\\turl_slides = {https://leventebajczi.com/publications/slides/tacas24etheta.pdf},\\n\\turl_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. F.\",\"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://csanadtelbisz.github.io/publications/tacas24etheta.pdf\",\" slides\":\"https://leventebajczi.com/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\":\"Theta: Abstraction Based Techniques for Verifying Concurrency (Competition Contribution)\",\"author\":[{\"propositions\":[],\"lastnames\":[\"Bajczi\"],\"firstnames\":[\"Levente\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Telbisz\"],\"firstnames\":[\"Csanád\",\"Ferenc\"],\"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\":[]}],\"doi\":\"10.1007/978-3-031-57256-2_30\",\"journal-iso\":\"LNCS\",\"journal\":\"LECTURE NOTES IN COMPUTER SCIENCE\",\"volume\":\"14572\",\"unique-id\":\"34768428\",\"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 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\",\"eissn\":\"1611-3349\",\"pages\":\"412-417\",\"orcid-numbers\":\"Bajczi, Levente/0000-0002-6551-5860; Telbisz, Csanád Ferenc/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://csanadtelbisz.github.io/publications/tacas24theta.pdf\",\"url_slides\":\"https://csanadtelbisz.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 Ferenc 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\\tdoi = {10.1007/978-3-031-57256-2_30},\\n\\tjournal-iso = {LNCS},\\n\\tjournal = {LECTURE NOTES IN COMPUTER SCIENCE},\\n\\tvolume = {14572},\\n\\tunique-id = {34768428},\\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 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\\teissn = {1611-3349},\\n\\tpages = {412-417},\\n\\torcid-numbers = {Bajczi, Levente/0000-0002-6551-5860; Telbisz, Csanád Ferenc/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\\t\\n\\turl_pdf = {https://csanadtelbisz.github.io/publications/tacas24theta.pdf},\\n\\turl_slides = {https://csanadtelbisz.github.io/publications/slides/tacas24theta.pdf},\\n\\turl_mtmt = {https://m2.mtmt.hu/api/publication/34768428},\\n}\",\"author_short\":[\"Bajczi, L.\",\"Telbisz, C. F.\",\"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://csanadtelbisz.github.io/publications/tacas24theta.pdf\",\" slides\":\"https://csanadtelbisz.github.io/publications/slides/tacas24theta.pdf\",\" mtmt\":\"https://m2.mtmt.hu/api/publication/34768428\"},\"metadata\":{\"authorlinks\":{\"bajczi, l\":\"https://leventebajczi.com/publications.html\"}},\"downloads\":8,\"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,QGFydGljbGV7TVRNVDozNjEyMjg5NywKCXRpdGxlID0ge09uIFN0YWJpbGl0eSBpbiBhIEhhcHBlbnMtQmVmb3JlIFByb3BhZ2F0b3IgZm9yIENvbmN1cnJlbnQgUHJvZ3JhbXMgKFJlcHJvZHVjaWJpbGl0eSBTdHVkeSl9LAoJYXV0aG9yID0ge0JhamN6aSwgTGV2ZW50ZSBhbmQgVGVsYmlzeiwgQ3NhbsOhZCBGZXJlbmMgYW5kIFN6ZWtlcmVzLCBEw6FuaWVsIGFuZCBWw7Zyw7ZzLCBBbmRyw6FzfSwKCWRvaSA9IHsxMC4xMDA3Lzk3OC0zLTAzMS05MDY0My01XzF9LAoJam91cm5hbC1pc28gPSB7TE5DU30sCglqb3VybmFsID0ge0xFQ1RVUkUgTk9URVMgSU4gQ09NUFVURVIgU0NJRU5DRX0sCgl2b2x1bWUgPSB7MTU2OTZ9LAoJdW5pcXVlLWlkID0gezM2MTIyODk3fSwKCWlzc24gPSB7MDMwMi05NzQzfSwKCWFic3RyYWN0ID0ge0FuYWx5emluZyBjb25jdXJyZW50IHByb2dyYW1zIG9mdGVuIGludm9sdmVzIHJlYXNvbmluZyBhYm91dCBoYXBwZW5zLWJlZm9yZSByZWxhdGlvbnMsIGhhbmRsZWQgYnkgZGVkaWNhdGVkIFNNVCB0aGVvcnkgc29sdmVycy4gUmVjZW50bHksIHByZXZlbnRhdGl2ZSBwcm9wYWdhdGlvbiBydWxlcyBoYXZlIGJlZW4gaW50cm9kdWNlZCBmb3IgY29uc2lzdGVuY3kgbW9kZWxzIHRvIGF2b2lkIHVubmVjZXNzYXJ5IGNvbXB1dGF0aW9ucy4gVGhpcyBwYXBlciBhbmFseXNlcyB0aGUgcmVwcm9kdWNpYmlsaXR5IG9mIGEgcmVjZW50bHkgcHVibGlzaGVkIHBhcGVyIHJlZ2FyZGluZyBhIGNvbmZsaWN0LWF2b2lkaW5nIGhhcHBlbnMtYmVmb3JlIHByb3BhZ2F0b3IuIFdlIHNob3cgdGhhdCB0aGUgdW5kZXJseWluZyBheGlvbXMgYXJlIGluc3VmZmljaWVudCBmb3Igc3VwcG9ydGluZyBzZXF1ZW50aWFsIGNvbnNpc3RlbmN5LiBXZSBmaW5kIHRoYXQgdGhlIGFsZ29yaXRobSBjYW4gbGVhdmUgb3V0IGNvbnN0cmFpbnRzIG9uIGV2ZW50IG9yZGVyaW5nIChldmVuIGNvbnNpZGVyaW5nIHRoZSBvcmlnaW5hbCBheGlvbXMpLCBpbXBhY3RpbmcgdGhlIGFjY3VyYWN5IG9mIHZlcmlmaWNhdGlvbi4gV2Ugc2hvdyBhIHNpbXBsZSBjb3VudGVyZXhhbXBsZSB0byB0aGUgc3RhYmlsaXR5IGNsYWltIGluIHRoZSBwYXBlci4gVHdvIHJldmlzaW9ucyBvZiB0aGUgYWxnb3JpdGhtIGFyZSBwcmVzZW50ZWQsIGFuZCBhIHByb29mIG9uIHRoZSBjb3JyZWN0bmVzcyBvZiB0aGVzZSBhcHByb2FjaGVzIHJlc3BlY3RpdmUgb2YgdGhlIG9yaWdpbmFsIGF4aW9tcyBpcyBzaG93bi4gVGhlIHRvb2wgaW1wbGVtZW50aW5nIHRoZSBvcmlnaW5hbCBhbGdvcml0aG0gaXMgZXhhbWluZWQgdG8gYXNjZXJ0YWluIGhvdyBpdCBjaXJjdW12ZW50cyB3cm9uZyByZXN1bHRzLiBJdCBpcyBmb3VuZCB0aGF0IGl0IGRldmlhdGVzIGZyb20gdGhlIHB1Ymxpc2hlZCBhbGdvcml0aG0uIFdlIHNob3cgdGhhdCBhbiB1bm1vZGlmaWVkIGFsZ29yaXRobSAodmlhIGEgcGF0Y2ggaW4gdGhlIGltcGxlbWVudGluZyB0b29sKSBjYXVzZXMgaW5jb3JyZWN0IHJlc3VsdHMuIFdlIGFsc28gc2hvdyB0aGF0IG91ciByZXZpc2VkIGFsZ29yaXRobSBjYW4gYmUgaW1wbGVtZW50ZWQgZWZmaWNpZW50bHkgaW4gYW4gaW5kZXBlbmRlbnQgdmVyaWZpY2F0aW9uIHRvb2wufSwKCXllYXIgPSB7MjAyNX0sCgllaXNzbiA9IHsxNjExLTMzNDl9LAoJcGFnZXMgPSB7My0xOX0sCglvcmNpZC1udW1iZXJzID0ge0JhamN6aSwgTGV2ZW50ZS8wMDAwLTAwMDItNjU1MS01ODYwOyBUZWxiaXN6LCBDc2Fuw6FkIEZlcmVuYy8wMDAwLTAwMDItNjI2MC01OTA4OyBTemVrZXJlcywgRMOhbmllbC8wMDAwLTAwMDItMjkxMi0wMjhYfSwKCQoJdXJsX3BkZiA9IHtodHRwczovL2NzYW5hZHRlbGJpc3ouZ2l0aHViLmlvL3B1YmxpY2F0aW9ucy90YWNhczI1b2NmaXgucGRmfSwKCXVybF9zbGlkZXMgPSB7aHR0cHM6Ly9sZXZlbnRlYmFqY3ppLmdpdGh1Yi5pby9wdWJsaWNhdGlvbnMvc2xpZGVzL3RhY2FzMjVvY2ZpeC5wZGZ9LAoJdXJsX210bXQgPSB7aHR0cHM6Ly9tMi5tdG10Lmh1L2FwaS9wdWJsaWNhdGlvbi8zNjEyMjg5N30sCn0KCgoKQGlucHJvY2VlZGluZ3N7TVRNVDozNjE3NjE5OSwKCXRpdGxlID0ge0dpdmluZyBTb21lIFBvaW50ZXJzIGZvciBBYnN0cmFjdGlvbi1CYXNlZCBNb2RlbCBDaGVja2luZ30sCglhdXRob3IgPSB7QmFqY3ppLCBMZXZlbnRlIGFuZCBTemVrZXJlcywgRMOhbmllbCBhbmQgVGVsYmlzeiwgQ3NhbsOhZCBGZXJlbmMgYW5kIE1vbG7DoXIsIFZpbmNlfSwKCWJvb2t0aXRsZSA9IHtQcm9jZWVkaW5ncyBvZiB0aGUgMzJuZCBNaW5pc3ltcG9zaXVtfSwKCWRvaSA9IHsxMC4zMzExL01JTklTWTIwMjUtMDAyfSwKCXVuaXF1ZS1pZCA9IHszNjE3NjE5OX0sCglhYnN0cmFjdCA9IHtBYnN0cmFjdGlvbi1iYXNlZCBzb2Z0d2FyZSBtb2RlbCBjaGVja2VycyBvZnRlbiByZWx5IG9uIGV4dGVybmFsIGFuYWx5c2VzIG9yIHVuYm91bmRlZCBTTVQgYXJyYXlzIHRvIHJlYXNvbiBhYm91dCBwb2ludGVycywgYXJyYXlzLCBhbmQgZHluYW1pYyBoZWFwIG1hbmlwdWxhdGlvbi4gRXh0ZXJuYWwgYW5hbHlzZXMgYXJlIHByZWNpc2UgYnV0IG9mdGVuIHJlcXVpcmUgdGhlIG1vZGlmaWNhdGlvbiBvZiBleGlzdGluZyB2ZXJpZmljYXRpb24gYWxnb3JpdGhtcywgd2hpbGUgU01UIGFycmF5cyBwcm92aWRlIGEgbmF0aXZlIHNvbHV0aW9uIGZvciBzb2x2ZXItYmFzZWQgdmVyaWZpZXJzIGJ1dCByZXF1aXJlIHN0cmljdCB0eXBlIHNhZmV0eSBvZnRlbiBmb3Jnb25lIGluIHJlYWwtd29ybGQgcHJvZ3JhbXMuIFdlIHByb3Bvc2UgYSBub3ZlbCB3YXkgb2YgaW50ZWdyYXRpbmcgYSBwcmVjaXNlIHBvaW50ZXIgYW5kIGFycmF5IGFuYWx5c2lzIGFzIGEgcGx1Zy1pbiBmb3IgYWJzdHJhY3Rpb24tYmFzZWQgbW9kZWwgY2hlY2tpbmcsIHdoaWNoIGRvZXMgbm90IHJlcXVpcmUgdGhlIG1vZGlmaWNhdGlvbiBvZiB0aGUgdW5kZXJseWluZyBhbGdvcml0aG1zLiBPdXIgc29sdXRpb24ga2VlcHMgdHJhY2sgb2YgYXJiaXRyYXJ5IHByZWRpY2F0ZXMgb3ZlciBwb3RlbnRpYWxseSBhYnN0cmFjdCBtZW1vcnkgbG9jYXRpb25zLCBtb3ZpbmcgdG93YXJkIG1vcmUgZWZmaWNpZW50IHZlcmlmaWNhdGlvbiBvZiBzb2Z0d2FyZSBjb2RlIGJ5IGFsbG93aW5nIGEgZmluZS1ncmFpbmVkIGFuZCBwcmVjaXNlIGFic3RyYWN0aW9uIG9mIG1lbW9yeSBhY2Nlc3Nlcy59LAoJeWVhciA9IHsyMDI1fSwKCXBhZ2VzID0gezUtOX0sCglvcmNpZC1udW1iZXJzID0ge0JhamN6aSwgTGV2ZW50ZS8wMDAwLTAwMDItNjU1MS01ODYwOyBTemVrZXJlcywgRMOhbmllbC8wMDAwLTAwMDItMjkxMi0wMjhYOyBUZWxiaXN6LCBDc2Fuw6FkIEZlcmVuYy8wMDAwLTAwMDItNjI2MC01OTA4OyBNb2xuw6FyLCBWaW5jZS8wMDAwLTAwMDItODIwNC03NTk1fSwKCQoJdXJsX3BkZiA9IHtodHRwczovL2NzYW5hZHRlbGJpc3ouZ2l0aHViLmlvL3B1YmxpY2F0aW9ucy9taW5pc3kyNXBvaW50ZXJzLnBkZn0sCgl1cmxfbXRtdCA9IHtodHRwczovL20yLm10bXQuaHUvYXBpL3B1YmxpY2F0aW9uLzM2MTc2MTk5fSwKfQoKCgpAaW5wcm9jZWVkaW5nc3tNVE1UOjM2MTIyODg1LAoJdGl0bGUgPSB7VGhldGE6IFZhcmlvdXMgQXBwcm9hY2hlcyBmb3IgQ29uY3VycmVudCBQcm9ncmFtIFZlcmlmaWNhdGlvbiAoQ29tcGV0aXRpb24gQ29udHJpYnV0aW9uKX0sCglhdXRob3IgPSB7VGVsYmlzeiwgQ3NhbsOhZCBGZXJlbmMgYW5kIEJhamN6aSwgTGV2ZW50ZSBhbmQgU3pla2VyZXMsIETDoW5pZWwgYW5kIFbDtnLDtnMsIEFuZHLDoXN9LAoJZG9pID0gezEwLjEwMDcvOTc4LTMtMDMxLTkwNjYwLTJfMjJ9LAoJam91cm5hbC1pc28gPSB7TE5DU30sCglqb3VybmFsID0ge0xFQ1RVUkUgTk9URVMgSU4gQ09NUFVURVIgU0NJRU5DRX0sCgl2b2x1bWUgPSB7MTU2OTh9LAoJdW5pcXVlLWlkID0gezM2MTIyODg1fSwKCWlzc24gPSB7MDMwMi05NzQzfSwKCWFic3RyYWN0ID0ge1RoZXRhIGlzIGEgbW9kZWwgY2hlY2tpbmcgZnJhbWV3b3JrIHdpdGggYSBzdHJvbmcgZW1waGFzaXMgb24gZWZmZWN0aXZlbHkgaGFuZGxpbmcgY29uY3VycmVuY3kgaW4gc29mdHdhcmUgdXNpbmcgYWJzdHJhY3Rpb24gcmVmaW5lbWVudCBhbGdvcml0aG1zLiBJbiBTVi1DT01QIDIwMjUsIHdlIGNvbXBsZW1lbnQgb3VyIGV4aXN0aW5nIGFwcHJvYWNoIChhYnN0cmFjdGlvbi1hd2FyZSBwYXJ0aWFsIG9yZGVyIHJlZHVjdGlvbikgZm9yIG11bHRpLXRocmVhZGVkIHByb2dyYW1zIHdpdGggYSBoYXBwZW5zIGJlZm9yZSBwcm9wYWdhdG9yLWJhc2VkIEJNQyBjaGVjaywgZXhwZWN0aW5nIGEgc2lnbmlmaWNhbnQgaW5jcmVhc2UgaW4gcGVyZm9ybWFuY2UuIFdlIGFnYWluIHV0aWxpemUgb3VyIHBvcnRmb2xpbyB3aXRoIGR5bmFtaWMgYWxnb3JpdGhtIHNlbGVjdGlvbiBmcm9tIGxhc3QgeWVhciwgd2l0aCBpbXByb3ZlbWVudHMgcmVnYXJkaW5nIHNvbHZlciBjaG9pY2UgYW5kIGNvbmZpZ3VyYXRpb24gb3JkZXJpbmcuIEluIHRoaXMgcGFwZXIsIHdlIGRldGFpbCBvdXIgYWxnb3JpdGhtaWMgaW1wcm92ZW1lbnRzIGluIFRoZXRhIHJlZ2FyZGluZyB0aGUgdmVyaWZpY2F0aW9uIG9mIGNvbmN1cnJlbnQgc29mdHdhcmUufSwKCXllYXIgPSB7MjAyNX0sCgllaXNzbiA9IHsxNjExLTMzNDl9LAoJcGFnZXMgPSB7MjYwLTI2NX0sCglvcmNpZC1udW1iZXJzID0ge1RlbGJpc3osIENzYW7DoWQgRmVyZW5jLzAwMDAtMDAwMi02MjYwLTU5MDg7IEJhamN6aSwgTGV2ZW50ZS8wMDAwLTAwMDItNjU1MS01ODYwOyBTemVrZXJlcywgRMOhbmllbC8wMDAwLTAwMDItMjkxMi0wMjhYfSwKCQoJdXJsX3BkZiA9IHtodHRwczovL2NzYW5hZHRlbGJpc3ouZ2l0aHViLmlvL3B1YmxpY2F0aW9ucy90YWNhczI1dGhldGEucGRmfSwKCXVybF9zbGlkZXMgPSB7aHR0cHM6Ly9jc2FuYWR0ZWxiaXN6LmdpdGh1Yi5pby9wdWJsaWNhdGlvbnMvc2xpZGVzL3RhY2FzMjV0aGV0YS5wZGZ9LAoJdXJsX210bXQgPSB7aHR0cHM6Ly9tMi5tdG10Lmh1L2FwaS9wdWJsaWNhdGlvbi8zNjEyMjg4NX0sCn0KCgoKQGlucHJvY2VlZGluZ3N7TVRNVDozNjI2NzE4NCwKCXRpdGxlID0ge1JlYXNvbmluZyB3aXRoIEhhcHBlbnMtQmVmb3JlIFJlbGF0aW9ucyBBYm91dCBDb25jdXJyZW50IFByb2dyYW1zIGluIHRoZSBUSEVUQSBGcmFtZXdvcmt9LAoJYXV0aG9yID0ge1RlbGJpc3osIENzYW7DoWQgRmVyZW5jIGFuZCBCYWpjemksIExldmVudGUgYW5kIFN6ZWtlcmVzLCBEw6FuaWVsIGFuZCBWw7Zyw7ZzLCBBbmRyw6FzIGFuZCBNYWp6aWssIElzdHbDoW59LAoJYm9va3RpdGxlID0gezIwMjUgNTV0aCBBbm51YWwgSUVFRS9JRklQIEludGVybmF0aW9uYWwgQ29uZmVyZW5jZSBvbiBEZXBlbmRhYmxlIFN5c3RlbXMgYW5kIE5ldHdvcmtzIFdvcmtzaG9wcyAoRFNOLVcpfSwKCWRvaSA9IHsxMC4xMTA5L0RTTi1XNjU3OTEuMjAyNS4wMDAzN30sCgl1bmlxdWUtaWQgPSB7MzYyNjcxODR9LAoJYWJzdHJhY3QgPSB7VGhlIG1vZGVsIGNoZWNraW5nIG9mIG11bHRpLXRocmVhZGVkIHByb2dyYW1zIG9mdGVuIGludm9sdmVzIHJlYXNvbmluZyBhYm91dCB0aGUgaGFwcGVucy1iZWZvcmUgcmVsYXRpb24gb2YgY29uY3VycmVudCBwcm9ncmFtIGluc3RydWN0aW9ucy4gU2V2ZXJhbCBhbGdvcml0aG1zIGV4aXN0IGZvciBmaW5kaW5nIGEgcGFydGlhbCBvcmRlciBvZiBpbnN0cnVjdGlvbnMgdGhhdCBpcyBjb25zaXN0ZW50IHdpdGggb3JkZXJpbmcgY29uc3RyYWludHMgb2YgdGhlIGFzc3VtZWQgbWVtb3J5IG1vZGVsIGFuZCB0aGF0IHZpb2xhdGVzIGEgc2FmZXR5IHByb3BlcnR5OyBvciBmb3IgcHJvdmluZyB0aGF0IHN1Y2ggcGFydGlhbCBvcmRlcnMgZG8gbm90IGV4aXN0LiBXZSBwcmVzZW50IGV4aXN0aW5nIGFuZCBub3ZlbCBib3VuZGVkIG1vZGVsIGNoZWNraW5nIGFwcHJvYWNoZXMgcmVhc29uaW5nIHdpdGggaGFwcGVucy1iZWZvcmUgcmVsYXRpb25zIG9mIGNvbmN1cnJlbnQgcHJvZ3JhbXMuIFRoZXNlIGFsZ29yaXRobXMgYXJlIGltcGxlbWVudGVkIGluIFRIRVRBLCBhIG1vZHVsYXIgbW9kZWwgY2hlY2tpbmcgZnJhbWV3b3JrLiBXZSBhbHNvIGdpdmUgYSBjb21wYXJhdGl2ZSBldmFsdWF0aW9uIG9mIG91ciBUSEVUQSBpbXBsZW1lbnRhdGlvbnMgYW5kIHN0YXRlLW9mLXRoZS1hcnQgdmVyaWZpZXJzLn0sCgl5ZWFyID0gezIwMjV9LAoJcGFnZXMgPSB7NDMtNDZ9LAoJb3JjaWQtbnVtYmVycyA9IHtUZWxiaXN6LCBDc2Fuw6FkIEZlcmVuYy8wMDAwLTAwMDItNjI2MC01OTA4OyBCYWpjemksIExldmVudGUvMDAwMC0wMDAyLTY1NTEtNTg2MDsgU3pla2VyZXMsIETDoW5pZWwvMDAwMC0wMDAyLTI5MTItMDI4WH0sCgkKCXVybF9wZGYgPSB7aHR0cHM6Ly9jc2FuYWR0ZWxiaXN6LmdpdGh1Yi5pby9wdWJsaWNhdGlvbnMvdmVyZGkyNW9jLnBkZn0sCgl1cmxfbXRtdCA9IHtodHRwczovL20yLm10bXQuaHUvYXBpL3B1YmxpY2F0aW9uLzM2MjY3MTg0fSwKfQoKCgpAaW5wcm9jZWVkaW5nc3tNVE1UOjM0NzY4NDIyLAoJdGl0bGUgPSB7RW1lcmdlblRoZXRhOiBWZXJpZmljYXRpb24gQmV5b25kIEFic3RyYWN0aW9uIFJlZmluZW1lbnQgKENvbXBldGl0aW9uIENvbnRyaWJ1dGlvbil9LAoJYXV0aG9yID0ge0JhamN6aSwgTGV2ZW50ZSBhbmQgU3pla2VyZXMsIETDoW5pZWwgYW5kIE1vbmRvaywgTWlsw6FuIGFuZCDDgWTDoW0sIFpzw7NmaWEgYW5kIFNvbW9yamFpLCBNw6FyayBhbmQgVGVsYmlzeiwgQ3NhbsOhZCBGZXJlbmMgYW5kIERvYm9zLUtvdsOhY3MsIE1paMOhbHkgYW5kIE1vbG7DoXIsIFZpbmNlfSwKCWRvaSA9IHsxMC4xMDA3Lzk3OC0zLTAzMS01NzI1Ni0yXzIzfSwKCWpvdXJuYWwtaXNvID0ge0xOQ1N9LAoJam91cm5hbCA9IHtMRUNUVVJFIE5PVEVTIElOIENPTVBVVEVSIFNDSUVOQ0V9LAoJdm9sdW1lID0gezE0NTcyfSwKCXVuaXF1ZS1pZCA9IHszNDc2ODQyMn0sCglpc3NuID0gezAzMDItOTc0M30sCglhYnN0cmFjdCA9IHtUaGV0YSBpcyBhIG1vZGVsIGNoZWNraW5nIGZyYW1ld29yayBjb252ZW50aW9uYWxseSBiYXNlZCBvbiBhYnN0cmFjdGlvbiByZWZpbmVtZW50IHRlY2huaXF1ZXMuIFdoaWxlIGFic3RyYWN0aW9uIGlzIHVzZWZ1bCBmb3IgYSBsYXJnZSBudW1iZXIgb2YgdmVyaWZpY2F0aW9uIHByb2JsZW1zLCB0aGUgb3Zlci1yZWxpYW5jZSBvbiB0aGUgdGVjaG5pcXVlIGxlZCB0byBUaGV0YSBiZWluZyB1bmFibGUgdG8gbWVhbmluZ2Z1bGx5IGFkYXB0LiBJZGVudGlmeWluZyB0aGlzIHByb2JsZW0gaW4gcHJldmlvdXMgeWVhcnMgb2YgU1YtQ09NUCBoYXMgbGVkIHVzIHRvIGNyZWF0ZSBFbWVyZ2VuVGhldGEgLCBhIHNhbmRib3ggZm9yIHRoZSBuZXcgYXBwcm9hY2hlcyB3ZSB3YW50IFRoZXRhIHRvIHN1cHBvcnQuIEJ5IGRpZmZlcmVudGlhdGluZyBiZXR3ZWVuIG1hdHVyZSBhbmQgZW1lcmdpbmcgdGVjaG5pcXVlcywgd2UgY2FuIGV4cGVyaW1lbnQgbW9yZSBmcmVlbHkgd2l0aG91dCBodXJ0aW5nIHRoZSByZWxpYWJpbGl0eSBvZiB0aGUgb3ZlcmFsbCBmcmFtZXdvcmsuIEluIHRoaXMgcGFwZXIgd2UgZGV0YWlsIHRoZSBkZXZlbG9wbWVudCByb3V0ZSB0byBFbWVyZ2VuVGhldGEgLCBhbmQgaXRzIGZpcnN0IGRlYnV0IG9uIFNWLUNPTVDigJkyNCBpbiB0aGUgUmVhY2hTYWZldHkgY2F0ZWdvcnkufSwKCXllYXIgPSB7MjAyNH0sCgllaXNzbiA9IHsxNjExLTMzNDl9LAoJcGFnZXMgPSB7MzcxLTM3NX0sCglvcmNpZC1udW1iZXJzID0ge0JhamN6aSwgTGV2ZW50ZS8wMDAwLTAwMDItNjU1MS01ODYwOyBTemVrZXJlcywgRMOhbmllbC8wMDAwLTAwMDItMjkxMi0wMjhYOyBNb25kb2ssIE1pbMOhbi8wMDAwLTAwMDEtNTM5Ni0yMTcyOyDDgWTDoW0sIFpzw7NmaWEvMDAwMC0wMDAzLTIzNTQtMTc1MDsgVGVsYmlzeiwgQ3NhbsOhZCBGZXJlbmMvMDAwMC0wMDAyLTYyNjAtNTkwODsgRG9ib3MtS292w6FjcywgTWlow6FseS8wMDAwLTAwMDItMDA2NC0yOTY1OyBNb2xuw6FyLCBWaW5jZS8wMDAwLTAwMDItODIwNC03NTk1fSwKCQoJdXJsX3BkZiA9IHtodHRwczovL2NzYW5hZHRlbGJpc3ouZ2l0aHViLmlvL3B1YmxpY2F0aW9ucy90YWNhczI0ZXRoZXRhLnBkZn0sCgl1cmxfc2xpZGVzID0ge2h0dHBzOi8vbGV2ZW50ZWJhamN6aS5jb20vcHVibGljYXRpb25zL3NsaWRlcy90YWNhczI0ZXRoZXRhLnBkZn0sCgl1cmxfbXRtdCA9IHtodHRwczovL20yLm10bXQuaHUvYXBpL3B1YmxpY2F0aW9uLzM0NzY4NDIyfSwKfQoKCgpAaW5wcm9jZWVkaW5nc3tNVE1UOjM0NzY4NDI4LAoJdGl0bGUgPSB7VGhldGE6IEFic3RyYWN0aW9uIEJhc2VkIFRlY2huaXF1ZXMgZm9yIFZlcmlmeWluZyBDb25jdXJyZW5jeSAoQ29tcGV0aXRpb24gQ29udHJpYnV0aW9uKX0sCglhdXRob3IgPSB7QmFqY3ppLCBMZXZlbnRlIGFuZCBUZWxiaXN6LCBDc2Fuw6FkIEZlcmVuYyBhbmQgU29tb3JqYWksIE3DoXJrIGFuZCDDgWTDoW0sIFpzw7NmaWEgYW5kIERvYm9zLUtvdsOhY3MsIE1paMOhbHkgYW5kIFN6ZWtlcmVzLCBEw6FuaWVsIGFuZCBNb25kb2ssIE1pbMOhbiBhbmQgTW9sbsOhciwgVmluY2V9LAoJZG9pID0gezEwLjEwMDcvOTc4LTMtMDMxLTU3MjU2LTJfMzB9LAoJam91cm5hbC1pc28gPSB7TE5DU30sCglqb3VybmFsID0ge0xFQ1RVUkUgTk9URVMgSU4gQ09NUFVURVIgU0NJRU5DRX0sCgl2b2x1bWUgPSB7MTQ1NzJ9LAoJdW5pcXVlLWlkID0gezM0NzY4NDI4fSwKCWlzc24gPSB7MDMwMi05NzQzfSwKCWFic3RyYWN0ID0ge1RoZXRhIGlzIGEgbW9kZWwgY2hlY2tpbmcgZnJhbWV3b3JrLCB3aXRoIGEgc3Ryb25nIGVtcGhhc2lzIG9uIGVmZmVjdGl2ZWx5IGhhbmRsaW5nIGNvbmN1cnJlbmN5IGluIHNvZnR3YXJlIHVzaW5nIGFic3RyYWN0aW9uIHJlZmluZW1lbnQgYWxnb3JpdGhtcy4gSW4gU1YtQ09NUCAyMDI0LCB3ZSB1c2UgMSkgYW4gYWJzdHJhY3Rpb24tYXdhcmUgcGFydGlhbCBvcmRlciByZWR1Y3Rpb247IDIpIGEgZHluYW1pYyBzdGF0ZW1lbnQgcmVkdWN0aW9uIHRlY2huaXF1ZTsgYW5kIDMpIGVuaGFuY2VkIHN1cHBvcnQgZm9yIGNhbGwgc3RhY2tzIHRvIGhhbmRsZSByZWN1cnNpdmUgcHJvZ3JhbXMuIFdlIGludGVncmF0ZSB0aGVzZSB0ZWNobmlxdWVzIGluIGFuIGltcHJvdmVkIGFyY2hpdGVjdHVyZSB3aXRoIGluaGVyZW50IHN1cHBvcnQgZm9yIHBvcnRmb2xpby1iYXNlZCB2ZXJpZmljYXRpb24gdXNpbmcgZHluYW1pYyBhbGdvcml0aG0gc2VsZWN0aW9uLCB3aXRoIGEgZGl2ZXJzZSBzZWxlY3Rpb24gb2Ygc3VwcG9ydGVkIFNNVCBzb2x2ZXJzIGFzIHdlbGwuIEluIHRoaXMgcGFwZXIgd2UgZGV0YWlsIHRoZSBhZHZhbmNlcyBvZiBUaGV0YSByZWdhcmRpbmcgY29uY3VycmVudCBhbmQgcmVjdXJzaXZlIHNvZnR3YXJlIHN1cHBvcnQufSwKCXllYXIgPSB7MjAyNH0sCgllaXNzbiA9IHsxNjExLTMzNDl9LAoJcGFnZXMgPSB7NDEyLTQxN30sCglvcmNpZC1udW1iZXJzID0ge0JhamN6aSwgTGV2ZW50ZS8wMDAwLTAwMDItNjU1MS01ODYwOyBUZWxiaXN6LCBDc2Fuw6FkIEZlcmVuYy8wMDAwLTAwMDItNjI2MC01OTA4OyDDgWTDoW0sIFpzw7NmaWEvMDAwMC0wMDAzLTIzNTQtMTc1MDsgRG9ib3MtS292w6FjcywgTWlow6FseS8wMDAwLTAwMDItMDA2NC0yOTY1OyBTemVrZXJlcywgRMOhbmllbC8wMDAwLTAwMDItMjkxMi0wMjhYOyBNb25kb2ssIE1pbMOhbi8wMDAwLTAwMDEtNTM5Ni0yMTcyOyBNb2xuw6FyLCBWaW5jZS8wMDAwLTAwMDItODIwNC03NTk1fSwKCQoJdXJsX3BkZiA9IHtodHRwczovL2NzYW5hZHRlbGJpc3ouZ2l0aHViLmlvL3B1YmxpY2F0aW9ucy90YWNhczI0dGhldGEucGRmfSwKCXVybF9zbGlkZXMgPSB7aHR0cHM6Ly9jc2FuYWR0ZWxiaXN6LmdpdGh1Yi5pby9wdWJsaWNhdGlvbnMvc2xpZGVzL3RhY2FzMjR0aGV0YS5wZGZ9LAoJdXJsX210bXQgPSB7aHR0cHM6Ly9tMi5tdG10Lmh1L2FwaS9wdWJsaWNhdGlvbi8zNDc2ODQyOH0sCn0=\">\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://csanadtelbisz.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://csanadtelbisz.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%2Fcsanadtelbisz.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%2Fcsanadtelbisz.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%2Fcsanadtelbisz.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        (4)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\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://csanadtelbisz.github.io/publications/tacas25ocfix.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'bajczi-telbisz-szekeres-vrs-onstabilityinahappensbeforepropagatorforconcurrentprogramsreproducibilitystudy-2025', 'https://csanadtelbisz.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://csanadtelbisz.github.io/publications/tacas25ocfix.pdf\"\n     onclick=\"log_download('bajczi-telbisz-szekeres-vrs-onstabilityinahappensbeforepropagatorforconcurrentprogramsreproducibilitystudy-2025', 'https://csanadtelbisz.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  &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-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\t\n\turl_pdf = {https://csanadtelbisz.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},\n}\n\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  <div class=\"bibbase_paper\" id=\"bajczi-szekeres-telbisz-molnr-givingsomepointersforabstractionbasedmodelchecking-2025\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"https://csanadtelbisz.github.io/publications/minisy25pointers.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'bajczi-szekeres-telbisz-molnr-givingsomepointersforabstractionbasedmodelchecking-2025', 'https://csanadtelbisz.github.io/publications/minisy25pointers.pdf', event);\">\n    Giving Some Pointers for Abstraction-Based Model Checking.\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.; Telbisz, C. F.;  and Molnár, V.\n</span>\n\n  \n\n</span>\n\n  In <i>Proceedings of the 32nd Minisymposium</i>, pages 5-9,  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://csanadtelbisz.github.io/publications/minisy25pointers.pdf\"\n     onclick=\"log_download('bajczi-szekeres-telbisz-molnr-givingsomepointersforabstractionbasedmodelchecking-2025', 'https://csanadtelbisz.github.io/publications/minisy25pointers.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"Giving Some Pointers for Abstraction-Based Model Checking [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/36176199\"\n     onclick=\"log_download('bajczi-szekeres-telbisz-molnr-givingsomepointersforabstractionbasedmodelchecking-2025', 'https://m2.mtmt.hu/api/publication/36176199', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"Giving Some Pointers for Abstraction-Based Model Checking [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.3311/MINISY2025-002\"\n     onclick=\"log_download('bajczi-szekeres-telbisz-molnr-givingsomepointersforabstractionbasedmodelchecking-2025', 'http://doi.org/10.3311/MINISY2025-002', 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-telbisz-molnr-givingsomepointersforabstractionbasedmodelchecking-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-szekeres-telbisz-molnr-givingsomepointersforabstractionbasedmodelchecking-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;\">@inproceedings{MTMT:36176199,\n\ttitle = {Giving Some Pointers for Abstraction-Based Model Checking},\n\tauthor = {Bajczi, Levente and Szekeres, Dániel and Telbisz, Csanád Ferenc and Molnár, Vince},\n\tbooktitle = {Proceedings of the 32nd Minisymposium},\n\tdoi = {10.3311/MINISY2025-002},\n\tunique-id = {36176199},\n\tabstract = {Abstraction-based software model checkers often rely on external analyses or unbounded SMT arrays to reason about pointers, arrays, and dynamic heap manipulation. External analyses are precise but often require the modification of existing verification algorithms, while SMT arrays provide a native solution for solver-based verifiers but require strict type safety often forgone in real-world programs. We propose a novel way of integrating a precise pointer and array analysis as a plug-in for abstraction-based model checking, which does not require the modification of the underlying algorithms. Our solution keeps track of arbitrary predicates over potentially abstract memory locations, moving toward more efficient verification of software code by allowing a fine-grained and precise abstraction of memory accesses.},\n\tyear = {2025},\n\tpages = {5-9},\n\torcid-numbers = {Bajczi, Levente/0000-0002-6551-5860; Szekeres, Dániel/0000-0002-2912-028X; Telbisz, Csanád Ferenc/0000-0002-6260-5908; Molnár, Vince/0000-0002-8204-7595},\n\t\n\turl_pdf = {https://csanadtelbisz.github.io/publications/minisy25pointers.pdf},\n\turl_mtmt = {https://m2.mtmt.hu/api/publication/36176199},\n}\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  Abstraction-based software model checkers often rely on external analyses or unbounded SMT arrays to reason about pointers, arrays, and dynamic heap manipulation. External analyses are precise but often require the modification of existing verification algorithms, while SMT arrays provide a native solution for solver-based verifiers but require strict type safety often forgone in real-world programs. We propose a novel way of integrating a precise pointer and array analysis as a plug-in for abstraction-based model checking, which does not require the modification of the underlying algorithms. Our solution keeps track of arbitrary predicates over potentially abstract memory locations, moving toward more efficient verification of software code by allowing a fine-grained and precise abstraction of memory accesses.\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://csanadtelbisz.github.io/publications/tacas25theta.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'telbisz-bajczi-szekeres-vrs-thetavariousapproachesforconcurrentprogramverificationcompetitioncontribution-2025', 'https://csanadtelbisz.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  In volume 15698, pages 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://csanadtelbisz.github.io/publications/tacas25theta.pdf\"\n     onclick=\"log_download('telbisz-bajczi-szekeres-vrs-thetavariousapproachesforconcurrentprogramverificationcompetitioncontribution-2025', 'https://csanadtelbisz.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://csanadtelbisz.github.io/publications/slides/tacas25theta.pdf\"\n     onclick=\"log_download('telbisz-bajczi-szekeres-vrs-thetavariousapproachesforconcurrentprogramverificationcompetitioncontribution-2025', 'https://csanadtelbisz.github.io/publications/slides/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=\" 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/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  &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('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;\">@inproceedings{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\t\n\turl_pdf = {https://csanadtelbisz.github.io/publications/tacas25theta.pdf},\n\turl_slides = {https://csanadtelbisz.github.io/publications/slides/tacas25theta.pdf},\n\turl_mtmt = {https://m2.mtmt.hu/api/publication/36122885},\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=\"telbisz-bajczi-szekeres-vrs-majzik-reasoningwithhappensbeforerelationsaboutconcurrentprogramsinthethetaframework-2025\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"https://csanadtelbisz.github.io/publications/verdi25oc.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'telbisz-bajczi-szekeres-vrs-majzik-reasoningwithhappensbeforerelationsaboutconcurrentprogramsinthethetaframework-2025', 'https://csanadtelbisz.github.io/publications/verdi25oc.pdf', event);\">\n    Reasoning with Happens-Before Relations About Concurrent Programs in the THETA Framework.\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.; Vörös, A.;  and Majzik, I.\n</span>\n\n  \n\n</span>\n\n  In <i>2025 55th Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshops (DSN-W)</i>, pages 43-46,  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://csanadtelbisz.github.io/publications/verdi25oc.pdf\"\n     onclick=\"log_download('telbisz-bajczi-szekeres-vrs-majzik-reasoningwithhappensbeforerelationsaboutconcurrentprogramsinthethetaframework-2025', 'https://csanadtelbisz.github.io/publications/verdi25oc.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"Reasoning with Happens-Before Relations About Concurrent Programs in the THETA Framework [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/36267184\"\n     onclick=\"log_download('telbisz-bajczi-szekeres-vrs-majzik-reasoningwithhappensbeforerelationsaboutconcurrentprogramsinthethetaframework-2025', 'https://m2.mtmt.hu/api/publication/36267184', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"Reasoning with Happens-Before Relations About Concurrent Programs in the THETA Framework [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.1109/DSN-W65791.2025.00037\"\n     onclick=\"log_download('telbisz-bajczi-szekeres-vrs-majzik-reasoningwithhappensbeforerelationsaboutconcurrentprogramsinthethetaframework-2025', 'http://doi.org/10.1109/DSN-W65791.2025.00037', 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-majzik-reasoningwithhappensbeforerelationsaboutconcurrentprogramsinthethetaframework-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-majzik-reasoningwithhappensbeforerelationsaboutconcurrentprogramsinthethetaframework-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;\">@inproceedings{MTMT:36267184,\n\ttitle = {Reasoning with Happens-Before Relations About Concurrent Programs in the THETA Framework},\n\tauthor = {Telbisz, Csanád Ferenc and Bajczi, Levente and Szekeres, Dániel and Vörös, András and Majzik, István},\n\tbooktitle = {2025 55th Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshops (DSN-W)},\n\tdoi = {10.1109/DSN-W65791.2025.00037},\n\tunique-id = {36267184},\n\tabstract = {The model checking of multi-threaded programs often involves reasoning about the happens-before relation of concurrent program instructions. Several algorithms exist for finding a partial order of instructions that is consistent with ordering constraints of the assumed memory model and that violates a safety property; or for proving that such partial orders do not exist. We present existing and novel bounded model checking approaches reasoning with happens-before relations of concurrent programs. These algorithms are implemented in THETA, a modular model checking framework. We also give a comparative evaluation of our THETA implementations and state-of-the-art verifiers.},\n\tyear = {2025},\n\tpages = {43-46},\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\t\n\turl_pdf = {https://csanadtelbisz.github.io/publications/verdi25oc.pdf},\n\turl_mtmt = {https://m2.mtmt.hu/api/publication/36267184},\n}\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  The model checking of multi-threaded programs often involves reasoning about the happens-before relation of concurrent program instructions. Several algorithms exist for finding a partial order of instructions that is consistent with ordering constraints of the assumed memory model and that violates a safety property; or for proving that such partial orders do not exist. We present existing and novel bounded model checking approaches reasoning with happens-before relations of concurrent programs. These algorithms are implemented in THETA, a modular model checking framework. We also give a comparative evaluation of our THETA implementations and state-of-the-art verifiers.\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        (2)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\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://csanadtelbisz.github.io/publications/tacas24etheta.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'bajczi-szekeres-mondok-dm-somorjai-telbisz-doboskovcs-molnr-emergenthetaverificationbeyondabstractionrefinementcompetitioncontribution-2024', 'https://csanadtelbisz.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. F.; Dobos-Kovács, M.;  and Molnár, V.\n</span>\n\n  \n\n</span>\n\n  In volume 14572, 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://csanadtelbisz.github.io/publications/tacas24etheta.pdf\"\n     onclick=\"log_download('bajczi-szekeres-mondok-dm-somorjai-telbisz-doboskovcs-molnr-emergenthetaverificationbeyondabstractionrefinementcompetitioncontribution-2024', 'https://csanadtelbisz.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.com/publications/slides/tacas24etheta.pdf\"\n     onclick=\"log_download('bajczi-szekeres-mondok-dm-somorjai-telbisz-doboskovcs-molnr-emergenthetaverificationbeyondabstractionrefinementcompetitioncontribution-2024', 'https://leventebajczi.com/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 Ferenc and Dobos-Kovács, Mihály and Molnár, Vince},\n\tdoi = {10.1007/978-3-031-57256-2_23},\n\tjournal-iso = {LNCS},\n\tjournal = {LECTURE NOTES IN COMPUTER SCIENCE},\n\tvolume = {14572},\n\tunique-id = {34768422},\n\tissn = {0302-9743},\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\teissn = {1611-3349},\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 Ferenc/0000-0002-6260-5908; Dobos-Kovács, Mihály/0000-0002-0064-2965; Molnár, Vince/0000-0002-8204-7595},\n\t\n\turl_pdf = {https://csanadtelbisz.github.io/publications/tacas24etheta.pdf},\n\turl_slides = {https://leventebajczi.com/publications/slides/tacas24etheta.pdf},\n\turl_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-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://csanadtelbisz.github.io/publications/tacas24theta.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'bajczi-telbisz-somorjai-dm-doboskovcs-szekeres-mondok-molnr-thetaabstractionbasedtechniquesforverifyingconcurrencycompetitioncontribution-2024', 'https://csanadtelbisz.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. F.; 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 volume 14572, 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://csanadtelbisz.github.io/publications/tacas24theta.pdf\"\n     onclick=\"log_download('bajczi-telbisz-somorjai-dm-doboskovcs-szekeres-mondok-molnr-thetaabstractionbasedtechniquesforverifyingconcurrencycompetitioncontribution-2024', 'https://csanadtelbisz.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://csanadtelbisz.github.io/publications/slides/tacas24theta.pdf\"\n     onclick=\"log_download('bajczi-telbisz-somorjai-dm-doboskovcs-szekeres-mondok-molnr-thetaabstractionbasedtechniquesforverifyingconcurrencycompetitioncontribution-2024', 'https://csanadtelbisz.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>8 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 Ferenc 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\tdoi = {10.1007/978-3-031-57256-2_30},\n\tjournal-iso = {LNCS},\n\tjournal = {LECTURE NOTES IN COMPUTER SCIENCE},\n\tvolume = {14572},\n\tunique-id = {34768428},\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 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\teissn = {1611-3349},\n\tpages = {412-417},\n\torcid-numbers = {Bajczi, Levente/0000-0002-6551-5860; Telbisz, Csanád Ferenc/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\t\n\turl_pdf = {https://csanadtelbisz.github.io/publications/tacas24theta.pdf},\n\turl_slides = {https://csanadtelbisz.github.io/publications/slides/tacas24theta.pdf},\n\turl_mtmt = {https://m2.mtmt.hu/api/publication/34768428},\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\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);