TY - JOUR AU - Bajczi, Levente AU - Telbisz, Csanád Ferenc AU - Szekeres, Dániel AU - Vörös, András TI - On Stability in a Happens-Before Propagator for Concurrent Programs (Reproducibility Study) JF - LECTURE NOTES IN COMPUTER SCIENCE J2 - LNCS VL - 15696 PY - 2025 SP - 3 EP - 19 PG - 17 SN - 0302-9743 DO - 10.1007/978-3-031-90643-5_1 UR - https://m2.mtmt.hu/api/publication/36122897 ID - 36122897 N1 - This research was partially funded by the EKÖP-24-{2,3} New National Excellence Program under project numbers EKÖP-24-2-BME-118, EKÖP-24-3-BME-213 and EKÖP-24-3-BME-159, and the Doctoral Excellence Fellowship Programme under project numbers 400434/2023, 400443/2023; funded by the NRDI Fund of Hungary. This work was partially supported by project no. 2022-1.2.4-EUREKA-2023-00013 under the 2022-1.2.4 EUREKA funding scheme from the the National Research, Development and Innovation Fund of Hungary. AB - 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. LA - English DB - MTMT ER - TY - JOUR AU - Dobos-Kovács, Mihály AU - Bajczi, Levente AU - Vörös, András TI - CHCVerif: A Portfolio-Based Solver for Constrained Horn Clauses JF - ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE J2 - ELECTRON PROC THEOR COMPUT SCI VL - 434 PY - 2025 SP - 40 EP - 51 PG - 12 SN - 2075-2180 DO - 10.4204/EPTCS.434.6 UR - https://m2.mtmt.hu/api/publication/36429902 ID - 36429902 LA - English DB - MTMT ER - TY - CHAP AU - Szabó, Richárd AU - Cziborová, Dóra AU - Vörös, András ED - Renczes, Balázs TI - Towards Configurable Coordination for Distributed Reactive Systems T2 - Proceedings of the 32nd Minisymposium PB - Budapest University of Technology and Economics, Department of Artificial Intelligence and Systems Engineering CY - Budapest SN - 9789634219897 PY - 2025 SP - 45 EP - 50 PG - 6 DO - 10.3311/MINISY2025-009 UR - https://m2.mtmt.hu/api/publication/36196264 ID - 36196264 LA - English DB - MTMT ER - TY - JOUR AU - Telbisz, Csanád Ferenc AU - Bajczi, Levente AU - Szekeres, Dániel AU - Vörös, András TI - Theta: Various Approaches for Concurrent Program Verification (Competition Contribution) JF - LECTURE NOTES IN COMPUTER SCIENCE J2 - LNCS VL - 15698 PY - 2025 SP - 260 EP - 265 PG - 6 SN - 0302-9743 DO - 10.1007/978-3-031-90660-2_22 UR - https://m2.mtmt.hu/api/publication/36122885 ID - 36122885 N1 - This research was partially funded by the EKÖP-24-{2,3} New National Excellence Program under project numbers EKÖP-24-2-BME-118, EKÖP-24-3-BME-213 and EKÖP-24-3-BME-159, and the Doctoral Excellence Fellowship Programme under project numbers 400434/2023 and 400443/2023; funded by the NRDI Fund of Hungary. AB - 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. LA - English DB - MTMT ER - TY - CHAP AU - Telbisz, Csanád Ferenc AU - Bajczi, Levente AU - Szekeres, Dániel AU - Vörös, András AU - Majzik, István ED - Cinque, Marcello ED - Cotroneo, Domenico ED - De Simone, Luigi ED - Eckhart, Matthias ED - Lee, Patrick P. C. ED - Zonouz, Saman TI - Reasoning with Happens-Before Relations About Concurrent Programs in the THETA Framework T2 - 2025 55th Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshops (DSN-W) PB - IEEE CY - Piscataway (NJ) SN - 9798331512057 T3 - Proceedings - International Conference on Dependable Systems and Networks Workshops, DSN-W, ISSN 2325-6648 PY - 2025 SP - 43 EP - 46 PG - 4 DO - 10.1109/DSN-W65791.2025.00037 UR - https://m2.mtmt.hu/api/publication/36267184 ID - 36267184 AB - 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. LA - English DB - MTMT ER - TY - JOUR AU - Telbisz, Csanád Ferenc AU - Bajczi, Levente AU - Szekeres, Dániel AU - Vörös, András TI - On-the-Fly Cone-of-Influence Reduction for Model Checking Concurrent Software JF - LECTURE NOTES IN COMPUTER SCIENCE J2 - LNCS VL - 15945 PY - 2025 SP - 161 EP - 181 PG - 21 SN - 0302-9743 DO - 10.1007/978-3-032-06847-7_9 UR - https://m2.mtmt.hu/api/publication/36411499 ID - 36411499 N1 - This research was partially funded by the 2024-2.1.1-EKÖP-2024-00003 University Research Scholarship Programme under project numbers EKÖP-24-2-BME-118 and EKÖP-24-3-BME-{159,213}, and the Doctoral Excellence Fellowship Programme under project numbers 400434/2023 and 400443/2023; with the support provided by the Ministry of Culture and Innovation of Hungary from the NRDI Fund. AB - 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. LA - English DB - MTMT ER - TY - CHAP AU - Molnár, Vince AU - Graics, Bence AU - Vörös, András AU - Tonetta, Stefano AU - Cristoforetti, Luca AU - Kimberly, Greg AU - Dyer, Pamela AU - Giammarco, Kristin AU - Koethe, Manfred AU - Hester, John AU - Smith, Jamie AU - Grimm, Christoph TI - Towards the Formal Verification of SysML v2 Models T2 - MODELS Companion '24: Proceedings of the ACM/IEEE 27th International Conference on Model Driven Engineering Languages and Systems PB - Association for Computing Machinery (ACM) CY - New York, New York SN - 9798400706226 PY - 2024 SP - 1086 EP - 1095 PG - 10 DO - 10.1145/3652620.3687820 UR - https://m2.mtmt.hu/api/publication/35500643 ID - 35500643 N1 - Funding Agency and Grant Number: German BMBF [2022-1.2.4-EUREKA-2023-00013, 2022-1.2.4-EUREKA] Funding text: We would like to thank every member of the Formal Methods Working Group who helped us write this paper with their insights and comments. We are also grateful to Ed Seidewitz and Conrad Bock, who never get tired of answering our questions. SysMD received support (GENIAL, KI4BoardNet) from the German BMBF. Gamma received support project no. 2022-1.2.4-EUREKA-2023-00013 under the 2022-1.2.4-EUREKA funding scheme. LA - English DB - MTMT ER - TY - JOUR AU - Somorjai, Márk AU - Dobos-Kovács, Mihály AU - Ádám, Zsófia AU - Bajczi, Levente AU - Vörös, András TI - Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification JF - ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE J2 - ELECTRON PROC THEOR COMPUT SCI VL - 402 PY - 2024 IS - 402 SP - 105 EP - 117 PG - 13 SN - 2075-2180 DO - 10.4204/EPTCS.402.11 UR - https://m2.mtmt.hu/api/publication/33784283 ID - 33784283 N1 - Conference code: 199105 Export Date: 10 May 2024 Funding details: Nemzeti Kutatási, Fejlesztési és Innovaciós Alap, NKFIA Funding text 1: Funding. This research was partially funded by the \\u00DANKP-22-{2,3}-I New National Excellence Program and the 2019-1.3.1-KK-2019-00004 project from the National Research, Development and Innovation Fund of Hungary. WoS:hiba:001313392600008 2025-03-21 06:13 DOI azonosító nem egyezik AB - 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. LA - English DB - MTMT ER - TY - CHAP AU - Dobos-Kovács, Mihály AU - Vörös, András ED - Anon, A TI - Evaluation of SMT solvers in abstraction-based software model checking T2 - Proceedings of the 11th Latin-American Symposium on Dependable Computing, LADC '22 PB - Association for Computing Machinery (ACM) CY - New York, New York SN - 9781450397377 PY - 2022 SP - 109 EP - 116 PG - 8 DO - 10.1145/3569902.3570187 UR - https://m2.mtmt.hu/api/publication/33575796 ID - 33575796 N1 - Export Date: 20 February 2023 LA - English DB - MTMT ER - TY - CHAP AU - Szabó, Richárd AU - Vörös, András ED - Renczes, Balázs TI - Dependability Modeling of Cyber-Physical Systems in the Gamma Framework T2 - Proceedings of the 29th Minisymposium of the Department of Measurement and Information Systems Budapest University of Technology and Economics PB - BME Méréstechnika és Információs Rendszerek Tanszék CY - Budapest SN - 9789634218722 PY - 2022 SP - 20 EP - 23 PG - 4 UR - https://m2.mtmt.hu/api/publication/32679018 ID - 32679018 LA - English DB - MTMT ER -