\n\n \n\n \n\n \n \n\n \n\n \n \n\n \n\n \n

\n generated by\n \n $\"bibbase.org\"\n$ \n \n

\n \n\n

\n\n

\n \n Group by\n \n \n
- \n Year\n
- \n Author\n
- \n Type\n
- \n Keyword\n
- \n Downloads\n
\n
\n \n \n \n \n
- \n \n Expand/Collapse All\n \n
- \n \n Download BibTeX\n \n
- \n \n RSS Feed\n \n
\n

\n\n\n

\n\n Excellent! Next you can\n create a new website with this list, or\n embed it in an existing web page by copying & pasting\n any of the following snippets.\n\n

\n JavaScript\n (easiest)\n

\n            <script src=\"https://bibbase.org/show?bib=https%3A%2F%2Fleventebajczi.github.io%2Fpublications.bib&jsonp=1&theme=side&jsonp=1\"></script>\n

\n\n PHP\n

\n            <?php\n            $contents = file_get_contents(\"https://bibbase.org/show?bib=https%3A%2F%2Fleventebajczi.github.io%2Fpublications.bib&jsonp=1&theme=side\");\n            print_r($contents);\n            ?>\n

\n\n iFrame\n (not recommended)\n

\n            <iframe src=\"https://bibbase.org/show?bib=https%3A%2F%2Fleventebajczi.github.io%2Fpublications.bib&jsonp=1&theme=side\"></iframe>\n

\n\n

\n For more details see the documention.\n

\n\n

\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 create a free account. 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

\n\n

To the site owner:

\n\n

Action required! Mendeley is changing its\n API. In order to keep using Mendeley with BibBase past April\n 14th, you need to:\n

renew the authorization for BibBase on Mendeley, and
update the BibBase URL\n in your page the same way you did when you initially set up\n this page.\n

\n\n

\n \n \n Fix it now\n

\n\n

\n\n\n

\n \n \n

\n \n 2025\n \n \n (10)\n \n \n

\n \n \n

\n \n\n \n \n \n \n \n \n NetworCat: applying analysis techniques of shared memory software on message-passing distributed systems.\n \n \n \n \n\n\n \n Bajczi, L.; and Molnár, V.\n\n\n \n\n\n\n SOFTWARE AND SYSTEMS MODELING. 2025.\n \n\n\n\n
\n\n\n\n \n \n $\"NetworCat:$ pdf\n \n \n \n $\"NetworCat:$ mtmt\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@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

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Theta: Various Approaches for Concurrent Program Verification (Competition Contribution).\n \n \n \n \n\n\n \n Telbisz, C. F.; Bajczi, L.; Szekeres, D.; and Vörös, A.\n\n\n \n\n\n\n LECTURE NOTES IN COMPUTER SCIENCE, 15698: 260-265. 2025.\n \n\n\n\n
\n\n\n\n \n \n $\"Theta:$ pdf\n \n \n \n $\"Theta:$ poster\n \n \n \n $\"Theta:$ mtmt\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 5 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@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

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n SV-COMP’25 Reproduction Report (Competition Contribution).\n \n \n \n \n\n\n \n Bajczi, L.; Ádám, Z.; and Micskei, Z. I.\n\n\n \n\n\n\n LECTURE NOTES IN COMPUTER SCIENCE, 15698: 187-191. 2025.\n \n\n\n\n
\n\n\n\n \n \n $\"SV-COMP’25$ pdf\n \n \n \n $\"SV-COMP’25$ slides\n \n \n \n $\"SV-COMP’25$ mtmt\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@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

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n EmergenTheta: Variations on Symbolic Transition Systems (Competition Contribution).\n \n \n \n \n\n\n \n Mondok, M.; Bajczi, L.; Szekeres, D.; and Molnár, V.\n\n\n \n\n\n\n LECTURE NOTES IN COMPUTER SCIENCE, 15698: 217-222. 2025.\n \n\n\n\n
\n\n\n\n \n \n $\"EmergenTheta:$ pdf\n \n \n \n $\"EmergenTheta:$ slides\n \n \n \n $\"EmergenTheta:$ mtmt\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@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

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n On Stability in a Happens-Before Propagator for Concurrent Programs (Reproducibility Study).\n \n \n \n \n\n\n \n Bajczi, L.; Telbisz, C. F.; Szekeres, D.; and Vörös, A.\n\n\n \n\n\n\n LECTURE NOTES IN COMPUTER SCIENCE, 15696: 3-19. 2025.\n \n\n\n\n
\n\n\n\n \n \n $\"On$ pdf\n \n \n \n $\"On$ slides\n \n \n \n $\"On$ mtmt\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@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}\n\n

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Giving Some Pointers for Abstraction-Based Model Checking.\n \n \n \n \n\n\n \n Bajczi, L.; Szekeres, D.; Telbisz, C. F.; and Molnár, V.\n\n\n \n\n\n\n In Proceedings of the 32nd Minisymposium, pages 5-9, 2025. \n \n\n\n\n
\n\n\n\n \n \n $\"Giving$ pdf\n \n \n \n $\"Giving$ slides\n \n \n \n $\"Giving$ mtmt\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 4 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@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\n\turl_pdf    = {https://leventebajczi.github.io/publications/minisy25ptr.pdf},\n\turl_slides = {https://leventebajczi.github.io/publications/slides/minisy25ptr.pdf},\n\turl_mtmt   = {https://m2.mtmt.hu/api/publication/36176199},\n}\n\n

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Theta as a Horn Solver.\n \n \n \n \n\n\n \n Bajczi, L.; Mondok, M.; and Molnár, V.\n\n\n \n\n\n\n ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 434: 27-39. 2025.\n \n\n\n\n
\n\n\n\n \n \n $\"Theta$ pdf\n \n \n \n $\"Theta$ slides\n \n \n \n $\"Theta$ mtmt\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{MTMT:36427979,\n\ttitle = {Theta as a Horn Solver},\n\tauthor = {Bajczi, Levente and Mondok, Milán and Molnár, Vince},\n\tdoi = {10.4204/EPTCS.434.5},\n\tjournal-iso = {ELECTRON PROC THEOR COMPUT SCI},\n\tjournal = {ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE},\n\tvolume = {434},\n\tunique-id = {36427979},\n\tabstract = {THETA is a verification framework that has participated in the CHC-COMP competition since 2023. While its core approach – based on transforming constrained Horn clauses (CHCs) into control-flow automata (CFAs) for analysis – has remained mostly unchanged, THETA’s verification techniques, design trade-offs, and limitations have remained mostly unexplored in the context of CHCs. This paper fills that gap: we provide a detailed description of the algorithms employed by Theta, highlighting the unique features that distinguish it from other CHC solvers. We also analyze the strengths and weaknesses of the tool in the context of CHC-COMP benchmarks. Notably, in the 2025 edition of the competition, Theta’s performance was impacted by a configuration issue, leading to suboptimal results. To provide a clearer picture of Theta’s actual capabilities, we re-execute the tool on the competition benchmarks under corrected settings and report on the resulting performance. © Bajczi et al.},\n\tyear = {2025},\n\teissn = {2075-2180},\n\tpages = {27-39},\n\torcid-numbers = {Bajczi, Levente/0000-0002-6551-5860; Mondok, Milán/0000-0001-5396-2172; Molnár, Vince/0000-0002-8204-7595},\n\n\turl_pdf    = {https://leventebajczi.github.io/publications/hcvs25theta.pdf},\n\turl_slides = {https://leventebajczi.github.io/publications/slides/hcvs25theta.pdf},\n\turl_mtmt   = {https://m2.mtmt.hu/api/publication/36427979},\n}\n\n

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n CHCVerif: A Portfolio-Based Solver for Constrained Horn Clauses.\n \n \n \n \n\n\n \n Dobos-Kovács, M.; Bajczi, L.; and Vörös, A.\n\n\n \n\n\n\n ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 434: 40-51. 2025.\n \n\n\n\n
\n\n\n\n \n \n $\"CHCVerif:$ pdf\n \n \n \n $\"CHCVerif:$ slides\n \n \n \n $\"CHCVerif:$ mtmt\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{MTMT:36429902,\n\ttitle = {CHCVerif: A Portfolio-Based Solver for Constrained Horn Clauses},\n\tauthor = {Dobos-Kovács, Mihály and Bajczi, Levente and Vörös, András},\n\tdoi = {10.4204/EPTCS.434.6},\n\tjournal-iso = {ELECTRON PROC THEOR COMPUT SCI},\n\tjournal = {ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE},\n\tvolume = {434},\n\tunique-id = {36429902},\n\tabstract = {Constrained Horn Clauses (CHCs) are widely adopted as intermediate representations for a variety of verification tasks, including safety checking, invariant synthesis, and inter procedural analysis. This paper introduces CHCVERIF, a portfolio-based CHC solver that adopts a software verification approach for solving CHCs. This approach enables us to reuse mature software verification tools to tackle CHC benchmarks, particularly those involving bitvectors and low-level semantics. Our evaluation shows that while the method enjoys only moderate success with linear integer arithmetic, it achieves modest success on bitvector benchmarks. Moreover, our results demonstrate the viability and potential of using software verification tools as backends for CHC solving, particularly when supported by a carefully constructed portfolio. © Dobos-Kovács et al.},\n\tyear = {2025},\n\teissn = {2075-2180},\n\tpages = {40-51},\n\torcid-numbers = {Dobos-Kovács, Mihály/0000-0002-0064-2965; Bajczi, Levente/0000-0002-6551-5860},\n\n\turl_pdf    = {https://leventebajczi.github.io/publications/hcvs25chcverif.pdf},\n\turl_slides = {https://leventebajczi.github.io/publications/slides/hcvs25chcverif.pdf},\n\turl_mtmt   = {https://m2.mtmt.hu/api/publication/36429902},\n}\n\n

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Reasoning with Happens-Before Relations About Concurrent Programs in the THETA Framework.\n \n \n \n \n\n\n \n Telbisz, C. F.; Bajczi, L.; Szekeres, D.; Vörös, A.; and Majzik, I.\n\n\n \n\n\n\n In 2025 55th Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshops (DSN-W), pages 43-46, 2025. \n \n\n\n\n
\n\n\n\n \n \n $\"Reasoning$ pdf\n \n \n \n $\"Reasoning$ slides\n \n \n \n $\"Reasoning$ mtmt\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@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\n\turl_pdf    = {https://leventebajczi.github.io/publications/verdi25oc.pdf},\n\turl_slides = {https://leventebajczi.github.io/publications/slides/verdi25oc.pdf},\n\turl_mtmt   = {https://m2.mtmt.hu/api/publication/36267184},\n}\n\n

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n On-the-Fly Cone-of-Influence Reduction for Model Checking Concurrent Software.\n \n \n \n \n\n\n \n Telbisz, C. F.; Bajczi, L.; Szekeres, D.; and Vörös, A.\n\n\n \n\n\n\n LECTURE NOTES IN COMPUTER SCIENCE, 15945: 161-181. 2025.\n \n\n\n\n
\n\n\n\n \n \n $\"On-the-Fly$ pdf\n \n \n \n $\"On-the-Fly$ mtmt\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{MTMT:36411499,\n\ttitle = {On-the-Fly Cone-of-Influence Reduction for Model Checking Concurrent Software},\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-032-06847-7_9},\n\tjournal-iso = {LNCS},\n\tjournal = {LECTURE NOTES IN COMPUTER SCIENCE},\n\tvolume = {15945},\n\tunique-id = {36411499},\n\tissn = {0302-9743},\n\tabstract = {Calculating successor states in SMT-based software model checking is a costly task that often requires solving an SMT problem. However, in many cases, the evaluation of a program statement has no effect with respect to the verified property. Successor state calculation can be simplified in such cases. Several algorithms exist such as the cone-of-influence reduction that statically analyze the model and eliminate irrelevant variables from the model. In concurrent software, however, it is common for the result of a statement to be used in one interleaving of threads while unused in another. Algorithms that statically analyze the model cannot simplify such statements. Our on-the-fly approach detects whether a statement can be simplified during the state space exploration based on the current state of each process. Evaluation results show that our algorithm can simplify around 20% of all statements on average over a large set of benchmark programs while reducing the time of successor state calculation by more than 30% on average.},\n\tyear = {2025},\n\teissn = {1611-3349},\n\tpages = {161-181},\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\turl_pdf    = {https://leventebajczi.github.io/publications/spin25coi.pdf},\n\turl_mtmt   = {https://m2.mtmt.hu/api/publication/36411499},\n}

\n\n\n\n\n\n

\n\n

\n \n 2024\n \n \n (7)\n \n \n

\n \n \n

\n \n\n \n \n \n \n \n \n ConcurrentWitness2Test: Test-Harnessing the Power of Concurrency (Competition Contribution).\n \n \n \n \n\n\n \n Bajczi, L.; Ádám, Z.; and Micskei, Z. I.\n\n\n \n\n\n\n In Tools and Algorithms for the Construction and Analysis of Systems, pages 330-334, 2024. \n \n\n\n\n
\n\n\n\n \n \n $\"ConcurrentWitness2Test:$ pdf\n \n \n \n $\"ConcurrentWitness2Test:$ slides\n \n \n \n $\"ConcurrentWitness2Test:$ mtmt\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 4 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@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

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Theta: Abstraction Based Techniques for Verifying Concurrency (Competition Contribution).\n \n \n \n \n\n\n \n Bajczi, L.; Telbisz, C.; Somorjai, M.; Ádám, Z.; Dobos-Kovács, M.; Szekeres, D.; Mondok, M.; and Molnár, V.\n\n\n \n\n\n\n In Tools and Algorithms for the Construction and Analysis of Systems, pages 412-417, 2024. \n \n\n\n\n
\n\n\n\n \n \n $\"Theta:$ pdf\n \n \n \n $\"Theta:$ slides\n \n \n \n $\"Theta:$ mtmt\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 9 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@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

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n EmergenTheta: Verification Beyond Abstraction Refinement (Competition Contribution).\n \n \n \n \n\n\n \n Bajczi, L.; Szekeres, D.; Mondok, M.; Ádám, Z.; Somorjai, M.; Telbisz, C.; Dobos-Kovács, M.; and Molnár, V.\n\n\n \n\n\n\n In Tools and Algorithms for the Construction and Analysis of Systems, pages 371-375, 2024. \n \n\n\n\n
\n\n\n\n \n \n $\"EmergenTheta:$ pdf\n \n \n \n $\"EmergenTheta:$ slides\n \n \n \n $\"EmergenTheta:$ mtmt\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@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

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Verbesserung der MBSE-Ausbildung durch Versionskontrolle und automatisiertes Feedback.\n \n \n \n \n\n\n \n Bajczi, L.; Szekeres, D.; Siegl, D.; and Molnár, V.\n\n\n \n\n\n\n In Tag des Systems Engineering, pages 161-169, 2024. \n \n\n\n\n
\n\n\n\n \n \n $\"Verbesserung$ pdf\n \n \n \n $\"Verbesserung$ slides\n \n \n \n $\"Verbesserung$ mtmt\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@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

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Enhancing MBSE Education with Version Control and Automated Feedback.\n \n \n \n \n\n\n \n Bajczi, L.; Szekeres, D.; Siegl, D.; and Molnár, V.\n\n\n \n\n\n\n 2024.\n \n\n\n\n
\n\n\n\n \n \n $\"Enhancing$ pdf\n \n \n \n $\"Enhancing$ slides\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@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

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification.\n \n \n \n \n\n\n \n Somorjai, M.; Dobos-Kovács, M.; Ádám, Z.; Bajczi, L.; and Vörös, A.\n\n\n \n\n\n\n ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 402: 105-117. 2024.\n \n\n\n\n
\n\n\n\n \n \n $\"Bottoms$ pdf\n \n \n \n $\"Bottoms$ mtmt\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@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

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Solving Constrained Horn Clauses as C Programs with CHC2C.\n \n \n \n \n\n\n \n Bajczi, L.; and Molnár, V.\n\n\n \n\n\n\n LECTURE NOTES IN COMPUTER SCIENCE, 14624: 146-163. 2024.\n \n\n\n\n
\n\n\n\n \n \n $\"Solving$ pdf\n \n \n \n $\"Solving$ slides\n \n \n \n $\"Solving$ mtmt\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n\n\n\n

@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

\n\n\n\n\n\n

\n\n

\n \n 2022\n \n \n (2)\n \n \n

\n \n \n

\n \n\n \n \n \n \n \n \n C for Yourself: Comparison of Front-End Techniques for Formal Verification.\n \n \n \n \n\n\n \n Bajczi, L.; Ádám, Z.; and Molnár, V.\n\n\n \n\n\n\n In 2022 IEEE/ACM 10th International Conference on Formal Methods in Software Engineering (FormaliSE), 2022. \n \n\n\n\n
\n\n\n\n \n \n $\"C$ pdf\n \n \n \n $\"C$ slides\n \n \n \n $\"C$ mtmt\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 7 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@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

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Theta: portfolio of CEGAR-based analyses with dynamic algorithm selection (Competition Contribution).\n \n \n \n \n\n\n \n Ádám, Z.; Bajczi, L.; Dobos-Kovács, M.; Hajdu, Á.; and Molnár, V.\n\n\n \n\n\n\n LECTURE NOTES IN COMPUTER SCIENCE, 13244: 474-478. 2022.\n \n\n\n\n
\n\n\n\n \n \n $\"Theta:$ pdf\n \n \n \n $\"Theta:$ slides\n \n \n \n $\"Theta:$ poster\n \n \n \n $\"Theta:$ mtmt\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 9 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n\n\n\n

@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

\n\n\n\n\n\n

\n\n

\n \n 2019\n \n \n (1)\n \n \n

\n \n \n

\n \n\n \n \n \n \n \n \n Will My Program Break on This Faulty Processor?. Formal Analysis of Hardware Fault Activations in Concurrent Embedded Software.\n \n \n \n \n\n\n \n Bajczi, L.; Vörös, A.; and Molnár, V.\n\n\n \n\n\n\n ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS, 18. 2019.\n \n\n\n\n
\n\n\n\n \n \n $\"Will$ pdf\n \n \n \n $\"Will$ slides\n \n \n \n $\"Will$ mtmt\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@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

\n\n\n\n\n\n

\n\n\n\n\n

\n\n\n \n\n \n \n \n \n\n