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 - CHAP AU - Szarvas, Dániel AU - Pogány, Domonkos TI - Conditional Molecule Generation with 2D Latent Diffusion T2 - Proceedings of the 31th Minisymposium PB - Budapest University of Technology and Economics CY - Budapest SN - 9789634219514 PY - 2024 SP - 37 EP - 40 PG - 4 DO - 10.3311/MINISY2024-007 UR - https://m2.mtmt.hu/api/publication/34862622 ID - 34862622 LA - English DB - MTMT ER - TY - CHAP AU - Pogány, Domonkos AU - Antal, Péter TI - Hyperbolic Drug-Target Interaction Prediction Utilizing Differential Expression Signatures T2 - Proceedings of the 31th Minisymposium PB - Budapest University of Technology and Economics CY - Budapest SN - 9789634219514 PY - 2024 SP - 46 EP - 49 PG - 4 DO - 10.3311/MINISY2024-009 UR - https://m2.mtmt.hu/api/publication/34862607 ID - 34862607 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 - CHAP AU - Kollár, Zsolt AU - Alrwashdeh, Monther AU - Leitold, László TI - Performance analysis of FBMC signals in the presence of DACs with limited range and resolution T2 - 2024 34th International Conference Radioelektronika (RADIOELEKTRONIKA) PB - IEEE SN - 9798350362169 PY - 2024 SP - 1 EP - 5 PG - 5 DO - 10.1109/RADIOELEKTRONIKA61599.2024.10524059 UR - https://m2.mtmt.hu/api/publication/34854562 ID - 34854562 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 - Eszlári, Nóra AU - Hullám, Gábor István AU - Gál, Zsófia AU - Török, Dóra AU - Nagy, Tamás AU - Millinghoffer, András Dániel AU - Baksa, Dániel AU - Gonda, Xénia AU - Antal, Péter AU - Bagdy, György AU - Juhász, Gabriella TI - Olfactory genes affect major depression in highly educated, emotionally stable, lean women: a bridge between animal models and precision medicine JF - TRANSLATIONAL PSYCHIATRY J2 - TRANSL PSYCHIAT VL - 14 PY - 2024 IS - 1 PG - 10 SN - 2158-3188 DO - 10.1038/s41398-024-02867-2 UR - https://m2.mtmt.hu/api/publication/34779723 ID - 34779723 N1 - Funding Agency and Grant Number: Hungarian National Research, Development, and Innovation Office [K 139330, K 143391, PD 146014, 2019-2.1.7-ERA-NET-2020-00005, ERAPERMED2019-108]; Hungarian Brain Research Program [2017-1.2.1-NKP-2017-00002]; Hungarian Brain Research Program 3.0 [NAP2022-I-4/2022, TKP2021-EGA-25]; Ministry of Innovation and Technology of Hungary National Research, Development and Innovation Fund [TKP2021-EGA-25]; National Research, Development, and Innovation Fund of Hungary [TKP2021-EGA-02]; European Union [RRF-2.3.1-21-2022-00004]; New National Excellence Program of the Ministry for Culture and Innovation National Research, Development and Innovation Fund [UNKP-23-4-II-SE-2]; Janos Bolyai Research Scholarship of the Hungarian Academy of Sciences; Semmelweis University; [UNKP-22-4-II-SE-1] Funding text: This study was supported by the Hungarian National Research, Development, and Innovation Office, with grants K 139330, K 143391, and PD 146014, as well as 2019-2.1.7-ERA-NET-2020-00005 under the frame of ERA PerMed (ERAPERMED2019-108); by the Hungarian Brain Research Program (grant: 2017-1.2.1-NKP-2017-00002) and the Hungarian Brain Research Program 3.0 (NAP2022-I-4/2022); and by TKP2021-EGA-25, implemented with the support provided by the Ministry of Innovation and Technology of Hungary from the National Research, Development and Innovation Fund, financed under the TKP2021-EGA funding scheme. It was also supported by the National Research, Development, and Innovation Fund of Hungary under Grant TKP2021-EGA-02 and the European Union project RRF-2.3.1-21-2022-00004 within the framework of the Artificial Intelligence National Laboratory. NE was supported by the UNKP-22-4-II-SE-1, and DB by the UNKP-23-4-II-SE-2 New National Excellence Program of the Ministry for Culture and Innovation from the source of the National Research, Development and Innovation Fund. NE is supported by the Janos Bolyai Research Scholarship of the Hungarian Academy of Sciences. This work uses data provided by patients and collected by the NHS as part of their care and support. Copyright (c) (2019), NHS England. Re-used with the permission of the UK Biobank (Application Number 1602). All rights reserved.Open access funding provided by Semmelweis University. AB - Most current approaches to establish subgroups of depressed patients for precision medicine aim to rely on biomarkers that require highly specialized assessment. Our present aim was to stratify participants of the UK Biobank cohort based on three readily measurable common independent risk factors, and to investigate depression genomics in each group to discover common and separate biological etiology. Two-step cluster analysis was run separately in males ( n = 149,879) and females ( n = 174,572), with neuroticism (a tendency to experience negative emotions), body fat percentage, and years spent in education as input variables. Genome-wide association analyses were implemented within each of the resulting clusters, for the lifetime occurrence of either a depressive episode or recurrent depressive disorder as the outcome. Variant-based, gene-based, gene set-based, and tissue-specific gene expression test were applied. Phenotypically distinct clusters with high genetic intercorrelations in depression genomics were found. A two-cluster solution was the best model in each sex with some differences including the less important role of neuroticism in males. In females, in case of a protective pattern of low neuroticism, low body fat percentage, and high level of education, depression was associated with pathways related to olfactory function. While also in females but in a risk pattern of high neuroticism, high body fat percentage, and less years spent in education, depression showed association with complement system genes. Our results, on one hand, indicate that alteration of olfactory pathways, that can be paralleled to the well-known rodent depression models of olfactory bulbectomy, might be a novel target towards precision psychiatry in females with less other risk factors for depression. On the other hand, our results in multi-risk females may provide a special case of immunometabolic depression. 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 -