TY - CHAP AU - Bajczi, Levente AU - Szekeres, Dániel AU - Siegl, Daniel AU - Molnár, Vince TI - Verbesserung der MBSE-Ausbildung durch Versionskontrolle und automatisiertes Feedback T2 - Tag des Systems Engineering PB - GfSE Verlag CY - Bremen SN - 9783910649057 PY - 2024 SP - 161 EP - 169 PG - 9 UR - https://m2.mtmt.hu/api/publication/35617761 ID - 35617761 LA - German DB - MTMT ER - TY - JOUR AU - Bajczi, Levente AU - Molnár, Vince TI - Solving Constrained Horn Clauses as C Programs with CHC2C JF - LECTURE NOTES IN COMPUTER SCIENCE J2 - LNCS VL - 14624 PY - 2024 SP - 146 EP - 163 PG - 18 SN - 0302-9743 DO - 10.1007/978-3-031-66149-5_8 UR - https://m2.mtmt.hu/api/publication/34853031 ID - 34853031 N1 - Softcover ISBN: 978-3-031-66148-8, Published: 13 October 2024; eBook ISBN: 978-3-031-66149-5, Published: 12 October 2024 Correspondence Address: Bajczi, L.; Department of Measurement and Information Systems, Hungary; email: bajczi@mit.bme.hu LA - English DB - MTMT ER - TY - JOUR AU - Bajczi, Levente AU - Ádám, Zsófia AU - Micskei, Zoltán Imre TI - ConcurrentWitness2Test: Test-Harnessing the Power of Concurrency (Competition Contribution) JF - LECTURE NOTES IN COMPUTER SCIENCE J2 - LNCS VL - 14572 PY - 2024 SP - 330 EP - 334 PG - 5 SN - 0302-9743 DO - 10.1007/978-3-031-57256-2_16 UR - https://m2.mtmt.hu/api/publication/34768972 ID - 34768972 AB - 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. LA - English DB - MTMT ER - TY - JOUR AU - Bajczi, Levente AU - Telbisz, Csanád Ferenc AU - Somorjai, Márk AU - Ádám, Zsófia AU - Dobos-Kovács, Mihály AU - Szekeres, Dániel AU - Mondok, Milán AU - Molnár, Vince TI - Theta: Abstraction Based Techniques for Verifying Concurrency (Competition Contribution) JF - LECTURE NOTES IN COMPUTER SCIENCE J2 - LNCS VL - 14572 PY - 2024 SP - 412 EP - 417 PG - 6 SN - 0302-9743 DO - 10.1007/978-3-031-57256-2_30 UR - https://m2.mtmt.hu/api/publication/34768428 ID - 34768428 AB - 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. LA - English DB - MTMT ER - TY - JOUR AU - Bajczi, Levente AU - Szekeres, Dániel AU - Mondok, Milán AU - Ádám, Zsófia AU - Somorjai, Márk AU - Telbisz, Csanád Ferenc AU - Dobos-Kovács, Mihály AU - Molnár, Vince TI - EmergenTheta: Verification Beyond Abstraction Refinement (Competition Contribution) JF - LECTURE NOTES IN COMPUTER SCIENCE J2 - LNCS VL - 14572 PY - 2024 SP - 371 EP - 375 PG - 5 SN - 0302-9743 DO - 10.1007/978-3-031-57256-2_23 UR - https://m2.mtmt.hu/api/publication/34768422 ID - 34768422 AB - 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. 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 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. 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 - JOUR AU - Ádám, Zsófia AU - Bajczi, Levente AU - Dobos-Kovács, Mihály AU - Hajdu, Ákos AU - Molnár, Vince TI - Theta: portfolio of CEGAR-based analyses with dynamic algorithm selection (Competition Contribution) JF - LECTURE NOTES IN COMPUTER SCIENCE J2 - LNCS VL - 13244 PY - 2022 SP - 474 EP - 478 PG - 5 SN - 0302-9743 DO - 10.1007/978-3-030-99527-0_34 UR - https://m2.mtmt.hu/api/publication/32801008 ID - 32801008 N1 - Chapter 34 Print ISBN978-3-030-99526-3 Online ISBN978-3-030-99527-0 LA - English DB - MTMT ER - TY - CHAP AU - Bajczi, Levente AU - Ádám, Zsófia AU - Molnár, Vince ED - Stefania, Gnesi ED - Nico, Plat TI - C for Yourself: Comparison of Front-End Techniques for Formal Verification T2 - FormaliSE '22: Proceedings of the IEEE/ACM 10th International Conference on Formal Methods in Software Engineering PB - Association for Computing Machinery (ACM) CY - New York, New York SN - 9781450392877 PY - 2022 SP - 1 EP - 11 PG - 11 DO - 10.1145/3524482.3527646 UR - https://m2.mtmt.hu/api/publication/32836583 ID - 32836583 N1 - Funding Agency and Grant Number: European Commission; Hungarian Authorities (NKFIH) [826452]; NKFIH grant [2019-2.1.3-NEMZ ECSEL-201900003]; New National Excellence Program of the Ministry for Innovation and Technology from the Source of the National Research, Development and Innovation Fund [UNKP-21-2-I-BME-142] Funding text: This research was partially funded by the European Commission and the Hungarian Authorities (NKFIH) through the Arrowhead Tools project (EU grant agreement No. 826452 (https://cordis.europa.eu/project/id/826452), NKFIH grant 2019-2.1.3-NEMZ ECSEL-201900003); and by the UNKP-21-2-I-BME-142 New National Excellence Program of the Ministry for Innovation and Technology from the Source of the National Research, Development and Innovation Fund. AB - 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. LA - English DB - MTMT ER - TY - JOUR AU - Bajczi, Levente AU - Vörös, András AU - Molnár, Vince TI - Will My Program Break on This Faulty Processor?. Formal Analysis of Hardware Fault Activations in Concurrent Embedded Software TS - Formal Analysis of Hardware Fault Activations in Concurrent Embedded Software JF - ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS J2 - ACM T EMBED COMPUT S VL - 18 PY - 2019 IS - 5 PG - 21 SN - 1539-9087 DO - 10.1145/3358238 UR - https://m2.mtmt.hu/api/publication/30865515 ID - 30865515 AB - 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. LA - English DB - MTMT ER -