@inproceedings{MTMT:35617761, title = {Verbesserung der MBSE-Ausbildung durch Versionskontrolle und automatisiertes Feedback}, url = {https://m2.mtmt.hu/api/publication/35617761}, author = {Bajczi, Levente and Szekeres, Dániel and Siegl, Daniel and Molnár, Vince}, booktitle = {Tag des Systems Engineering}, unique-id = {35617761}, year = {2024}, pages = {161-169}, orcid-numbers = {Bajczi, Levente/0000-0002-6551-5860; Szekeres, Dániel/0000-0002-2912-028X; Molnár, Vince/0000-0002-8204-7595} } @article{MTMT:34853031, title = {Solving Constrained Horn Clauses as C Programs with CHC2C}, url = {https://m2.mtmt.hu/api/publication/34853031}, author = {Bajczi, Levente and Molnár, Vince}, doi = {10.1007/978-3-031-66149-5_8}, journal-iso = {LNCS}, journal = {LECTURE NOTES IN COMPUTER SCIENCE}, volume = {14624}, unique-id = {34853031}, issn = {0302-9743}, year = {2024}, eissn = {1611-3349}, pages = {146-163}, orcid-numbers = {Bajczi, Levente/0000-0002-6551-5860; Molnár, Vince/0000-0002-8204-7595} } @article{MTMT:34768972, title = {ConcurrentWitness2Test: Test-Harnessing the Power of Concurrency (Competition Contribution)}, url = {https://m2.mtmt.hu/api/publication/34768972}, author = {Bajczi, Levente and Ádám, Zsófia and Micskei, Zoltán Imre}, doi = {10.1007/978-3-031-57256-2_16}, journal-iso = {LNCS}, journal = {LECTURE NOTES IN COMPUTER SCIENCE}, volume = {14572}, unique-id = {34768972}, issn = {0302-9743}, abstract = {ConcurrentWitness2Test is a violation witness validator for concurrent software. Taking both nondeterminism of data and interleaving-based nondeterminism into account, the tool aims to use the metadata described in the violation witnesses to synthesize an executable test harness. While plagued by some initial challenges yet to overcome, the validation performance of ConcurrentWitness2Test corroborates the usefulness of the proposed approach.}, year = {2024}, eissn = {1611-3349}, pages = {330-334}, orcid-numbers = {Bajczi, Levente/0000-0002-6551-5860; Ádám, Zsófia/0000-0003-2354-1750; Micskei, Zoltán Imre/0000-0003-1846-261X} } @article{MTMT:34768428, title = {Theta: Abstraction Based Techniques for Verifying Concurrency (Competition Contribution)}, url = {https://m2.mtmt.hu/api/publication/34768428}, author = {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}, 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} } @article{MTMT:34768422, title = {EmergenTheta: Verification Beyond Abstraction Refinement (Competition Contribution)}, url = {https://m2.mtmt.hu/api/publication/34768422}, author = {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}, 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} } @article{MTMT:33784283, title = {Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification}, url = {https://m2.mtmt.hu/api/publication/33784283}, author = {Somorjai, Márk and Dobos-Kovács, Mihály and Ádám, Zsófia and Bajczi, Levente and Vörös, András}, doi = {10.4204/EPTCS.402.11}, journal-iso = {ELECTRON PROC THEOR COMPUT SCI}, journal = {ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE}, volume = {402}, unique-id = {33784283}, abstract = {Constrained Horn Clauses (CHCs) have conventionally been used as a low-level representation in formal verification. Most existing solvers use a diverse set of specialized techniques, including direct state space traversal or under-approximating abstraction, necessitating purpose-built complex algorithms. Other solvers successfully simplified the verification workflow by translating the problem to inputs for other verification tasks, leveraging the strengths of existing algorithms. One such approach transforms the CHC problem into a recursive program roughly emulating a top-down solver for the deduction task; and verifying the reachability of a safety violation specified as a control location. We propose an alternative bottom-up approach for linear CHCs, and evaluate the two options in the open-source model checking framework THETA on both synthetic and industrial examples. We find that there is a more than twofold increase in the number of solved tasks when the novel bottom-up approach is used in the verification workflow, in contrast with the top-down technique. © Márk Somorjai et al.}, year = {2024}, eissn = {2075-2180}, pages = {105-117}, orcid-numbers = {Dobos-Kovács, Mihály/0000-0002-0064-2965; Ádám, Zsófia/0000-0003-2354-1750; Bajczi, Levente/0000-0002-6551-5860} } @article{MTMT:32801008, title = {Theta: portfolio of CEGAR-based analyses with dynamic algorithm selection (Competition Contribution)}, url = {https://m2.mtmt.hu/api/publication/32801008}, author = {Ádám, Zsófia and Bajczi, Levente and Dobos-Kovács, Mihály and Hajdu, Ákos and Molnár, Vince}, doi = {10.1007/978-3-030-99527-0_34}, journal-iso = {LNCS}, journal = {LECTURE NOTES IN COMPUTER SCIENCE}, volume = {13244}, unique-id = {32801008}, issn = {0302-9743}, keywords = {Computer Science, Software Engineering}, year = {2022}, eissn = {1611-3349}, pages = {474-478}, orcid-numbers = {Ádám, Zsófia/0000-0003-2354-1750; Bajczi, Levente/0000-0002-6551-5860; Dobos-Kovács, Mihály/0000-0002-0064-2965; Hajdu, Ákos/0000-0001-8001-8865; Molnár, Vince/0000-0002-8204-7595} } @inproceedings{MTMT:32836583, title = {C for Yourself: Comparison of Front-End Techniques for Formal Verification}, url = {https://m2.mtmt.hu/api/publication/32836583}, author = {Bajczi, Levente and Ádám, Zsófia and Molnár, Vince}, booktitle = {FormaliSE '22: Proceedings of the IEEE/ACM 10th International Conference on Formal Methods in Software Engineering}, doi = {10.1145/3524482.3527646}, unique-id = {32836583}, abstract = {With the improvement of hardware and algorithms, the main challenge of software model checking has shifted from pure algorithmic performance toward supporting a wider set of input programs. Successful toolchains tackle the problem of parsing a wide range of inputs in an efficient way by reusing solutions from existing compiler technologies such as Eclipse CDT or LLVM. Our experience suggests that well-established techniques in compiler technology are not necessarily beneficial to model checkers and sometimes can even hurt their performance. In this paper, we review the tools mature enough to participate in the Software Verification Competition in terms of the employed analysis and frontend techniques. We find that successful tools do exhibit a bias toward certain combinations. We explore the theoretical reasons and suggest an adaptable approach for model checking frameworks. We validate our recommendations by implementing a new frontend for a model checking framework and show that it indeed benefits some of the algorithms.}, keywords = {Model checking; formal verification; Computer Science, Software Engineering; Software model checking; CEGAR; BMC}, year = {2022}, pages = {1-11}, orcid-numbers = {Bajczi, Levente/0000-0002-6551-5860; Ádám, Zsófia/0000-0003-2354-1750; Molnár, Vince/0000-0002-8204-7595} } @article{MTMT:30865515, title = {Will My Program Break on This Faulty Processor?. Formal Analysis of Hardware Fault Activations in Concurrent Embedded Software}, url = {https://m2.mtmt.hu/api/publication/30865515}, author = {Bajczi, Levente and Vörös, András and Molnár, Vince}, doi = {10.1145/3358238}, journal-iso = {ACM T EMBED COMPUT S}, journal = {ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS}, volume = {18}, unique-id = {30865515}, issn = {1539-9087}, abstract = {Formal verification is approaching a point where it will be reliably applicable to embedded software. Even though formal verification can efficiently analyze multi-threaded applications, multi-core processors are often considered too dangerous to use in critical systems, despite the many benefits they can offer. One reason is the advanced memory consistency model of such CPUs. Nowadays, most software verifiers assume strict sequential consistency, which is also the naïve view of programmers. Modern multi-core processors, however, rarely guarantee this assumption by default. In addition, complex processor architectures may easily contain design faults. Thanks to the recent advances in hardware verification, these faults are increasingly visible and can be detected even in existing processors, giving an opportunity to compensate for the problem in software. In this paper, we propose a generic approach to consider inconsistent behavior of the hardware in the analysis of software. Our approach is based on formal methods and can be used to detect the activation of existing hardware faults on the application level and facilitate their mitigation in software. The approach relies heavily on recent results of model checking and hardware verification and offers new, integrative research directions. We propose a partial solution based on existing model checking tools to demonstrate feasibility and evaluate their performance in this context.}, year = {2019}, eissn = {1558-3465}, orcid-numbers = {Bajczi, Levente/0000-0002-6551-5860; Molnár, Vince/0000-0002-8204-7595} }