TY - CHAP AU - Cziborová, Dóra AU - Szabó, Richárd TI - Modeling of Time-Dependent Behavior in Fault-Tolerant Systems T2 - Proceedings of the 31th Minisymposium PB - Budapest University of Technology and Economics CY - Budapest SN - 9789634219514 PY - 2024 SP - 55 EP - 60 PG - 6 DO - 10.3311/MINISY2024-011 UR - https://m2.mtmt.hu/api/publication/34872818 ID - 34872818 LA - English DB - MTMT ER - TY - CHAP AU - Marussy, Kristóf AU - Ficsor, Attila AU - Semeráth, Oszkár AU - Varró, Dániel TI - Refinery: Graph Solver as a Service T2 - Proceedings of the 2024 IEEE/ACM 46th International Conference on Software Engineering: Companion Proceedings PB - Association for Computing Machinery (ACM) CY - New York, New York SN - 9798400705021 PY - 2024 SP - 64 EP - 68 PG - 5 DO - 10.1145/3639478.3640045 UR - https://m2.mtmt.hu/api/publication/34872599 ID - 34872599 LA - English DB - MTMT ER - TY - CHAP AU - Mondok, Milán AU - Molnár, Vince TI - Efficient Manipulation of Logical Formulas as Decision Diagrams T2 - Proceedings of the 31th Minisymposium PB - Budapest University of Technology and Economics CY - Budapest SN - 9789634219514 PY - 2024 SP - 61 EP - 65 PG - 5 UR - https://m2.mtmt.hu/api/publication/34869419 ID - 34869419 LA - English DB - MTMT ER - TY - CHAP AU - Péter, Bertalan Zoltán AU - Kocsis, Imre TI - Landmark Estimation for Qualitative Diagnosis Over Distributed Traces T2 - Proceedings of the 31th Minisymposium PB - Budapest University of Technology and Economics CY - Budapest SN - 9789634219514 PY - 2024 SP - 89 EP - 94 PG - 6 DO - 10.3311/MINISY2024-017 UR - https://m2.mtmt.hu/api/publication/34862731 ID - 34862731 LA - English DB - MTMT ER - TY - JOUR AU - Ádám, Zsófia AU - Beyer, Dirk AU - Chien, Po-Chun AU - Lee, Nian-Ze AU - Sirrenberg, Nils TI - Btor2-Cert: A Certifying Hardware-Verification Framework Using Software Analyzers JF - LECTURE NOTES IN COMPUTER SCIENCE J2 - LNCS VL - 14572 PY - 2024 SP - 129 EP - 149 PG - 21 SN - 0302-9743 DO - 10.1007/978-3-031-57256-2_7 UR - https://m2.mtmt.hu/api/publication/34860908 ID - 34860908 N1 - Department of Measurement and Information Systems, Budapest University of Technology and Economics, Budapest, Hungary Department of Computer Science, LMU Munich, Munich, Germany Conference code: 311189 Export Date: 17 May 2024 Correspondence Address: Beyer, D.; Department of Computer Science, Germany Funding details: Budapesti Műszaki és Gazdaságtudományi Egyetem, BME Funding details: Nemzeti Kutatási Fejlesztési és Innovációs Hivatal, NKFIH Funding details: Nemzeti Kutatási, Fejlesztési és Innovaciós Alap, NKFIA Funding details: Deutsche Forschungsgemeinschaft, DFG, 378803395 Funding details: Deutsche Forschungsgemeinschaft, DFG Funding text 1: Statement. This project was funded in part by the Deutsche Forschungsgemeinschaft (DFG) \\u2013 378803395 (ConVeY). Zs\\u00F3fia \\u00C1d\\u00E1m is supported partially by the Doctoral Excellence Fellowship Programme, which is funded by the National Research, Development and Innovation Fund of the Ministry of Culture and Innovation, and the Budapest University of Technology and Economics, under a grant agreement with the National Research, Development and Innovation Office. AB - Formal verification is essential but challenging: Even the best verifiers may produce wrong verification verdicts. Certifying verifiers enhance the confidence in verification results by generating a witness for other tools to validate the verdict independently. Recently, translating the hardware-modeling language Btor2 to software, such as the programming language C or LLVM intermediate representation, has been actively studied and facilitated verifying hardware designs by software analyzers. However, it remained unknown whether witnesses produced by software verifiers contain helpful information about the original circuits and how such information can aid hardware analysis. We propose a certifying and validating framework Btor2-Cert to verify safety properties of Btor2 circuits, combining Btor2-to-C translation, software verifiers, and a new witness validator Btor2-Val, to answer the above open questions. Btor2-Cert translates a software violation witness to a Btor2 violation witness; As the Btor2 language lacks a format for correctness witnesses, we encode invariants in software correctness witnesses as Btor2 circuits. The validator Btor2-Val checks violation witnesses by circuit simulation and correctness witnesses by validation via verification. In our evaluation, Btor2-Cert successfully utilized software witnesses to improve quality assurance of hardware. By invoking the software verifier Cbmc on translated programs, it uniquely solved, with confirmed witnesses, 8 % of the unsafe tasks for which the hardware verifier ABC failed to detect bugs. © The Author(s) 2024. LA - English 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 - Model Checking Software - 30th International Symposium, SPIN 2024, Luxembourg, Luxembourg, April 10-11, 2024, Proceedings PY - 2024 SN - 0302-9743 UR - https://m2.mtmt.hu/api/publication/34853031 ID - 34853031 LA - English DB - MTMT ER - TY - CHAP AU - Al-Gburi, Noor AU - Kocsis, Imre TI - Towards the Requirement-Driven Generation and Evaluation of Hyperledger Fabric Network Designs T2 - Proceedings of the 31th Minisymposium PB - Budapest University of Technology and Economics CY - Budapest SN - 9789634219514 PY - 2024 SP - 72 EP - 77 PG - 6 DO - 10.3311/MINISY2024-014 UR - https://m2.mtmt.hu/api/publication/34849521 ID - 34849521 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 -