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 - 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 - Csilla, Lea Fazekas AU - Manon, Bellardie AU - Bibiána, Török AU - Eszter, Sipos AU - Dobos-Kovács, Mihály AU - Elodie, Chaillou AU - Zelena, Dóra ED - Csiszár, Beáta ED - Hankó, Csilla ED - Kajos, Luca Fanni ED - Mező, Emerencia TI - Median raphe region serotoninergic neurones affect depressive-like behaviour and vegetative functions, but not social behaviour T2 - Medical Conference for PhD Students and Experts of Clinical Sciences 2021 PB - University of Pécs, Doctoral Student Association CY - Pécs SN - 9789634296539 PY - 2021 SP - 108 EP - 108 PG - 1 UR - https://m2.mtmt.hu/api/publication/32131082 ID - 32131082 LA - English DB - MTMT ER - TY - CHAP AU - Dobos-Kovács, Mihály AU - Hajdu, Ákos AU - Vörös, András ED - Andrey, Brito ED - Fernando, Pedone TI - Bitvector Support in the Theta Formal Verification Framework T2 - 2021 10th Latin-American Symposium on Dependable Computing (LADC) PB - Institute of Electrical and Electronics Engineers (IEEE) CY - Piscataway (NJ) SN - 9781665478311 PY - 2021 SP - 01 EP - 08 PG - 8 DO - 10.1109/LADC53747.2021.9672595 UR - https://m2.mtmt.hu/api/publication/32678888 ID - 32678888 LA - English DB - MTMT ER - TY - JOUR AU - Fazekas, Csilla Lea AU - Bellardie, M AU - Szocsics-Török, Bibiána AU - Bodóné Sipos, Eszter AU - Tóth, Blanka AU - Baranyi, Mária AU - Sperlágh, Beáta AU - Dobos-Kovács, Mihály AU - Chaillou, E AU - Zelena, Dóra TI - Pharmacogenetic excitation of the median raphe region affects social and depressive-like behavior and core body temperature in male mice JF - LIFE SCIENCES J2 - LIFE SCI VL - 286 PY - 2021 PG - 10 SN - 0024-3205 DO - 10.1016/j.lfs.2021.120037 UR - https://m2.mtmt.hu/api/publication/32399092 ID - 32399092 N1 - Institute of Experimental Medicine, Budapest, Hungary János Szentágothai Doctoral School of Neurosciences, Semmelweis University, Budapest, Hungary INRAE Centre Val de Loire, CNRS, IFCE, Université de Tours, UMR 85 Physiologie de la Reproduction et des Comportements, France Budapest University of Technology and Economics, Faculty of Chemical Technology and Biotechnology, Department of Inorganic and Analytical Chemistry, Budapest, Hungary Centre for Neuroscience, Szentágothai Research Centre, Institute of Physiology, Medical School, University of Pécs, Pécs, Hungary Cited By :7 Export Date: 10 September 2024 CODEN: LIFSA Correspondence Address: Fazekas, C.L.1083 Budapest, Szigony utca 43., Hungary; email: fazekas.csilla@koki.hu Chemicals/CAS: clozapine, 5786-21-0; clozapine n oxide, 34233-69-7; glutamic acid, 11070-68-1, 138-15-8, 56-86-0, 6899-05-4; Clozapine; clozapine N-oxide Funding details: K120311, K131406, TÉT_15-1-2016-003 Funding details: European Research Council, ERC, ERC-2011-ADG-294313 Funding text 1: This study was supported by European Research Council Advanced Research grant ( ERC-2011-ADG-294313 , SERRACO) and by the National Research Development and Innovation Office of Hungary (grant numbers K120311 , K131406 ) as well as by a bilateral Balaton Program ( TÉT_15-1-2016-003 ). None of the supporters had a further role in the study design; in the collection, analysis and interpretation of data; in the writing of the report; and in the decision to submit the paper for publication. LA - English DB - MTMT ER - TY - JOUR AU - Fazekas, Csilla Lea AU - Bellardie, Manon AU - Torok, Bibiana AU - Sipos, Eszter AU - Dobos-Kovács, Mihály AU - Chaillou, Elodie AU - Zelena, Dóra TI - The effect of median raphe region and its serotoninergic neurons on body temperature regulation in cold stress, depressive-like behaviour and social behaviour JF - JOURNAL OF NEURAL TRANSMISSION J2 - J NEURAL TRANSM VL - 128 PY - 2021 IS - 11 SP - 1779 EP - 1779 PG - 1 SN - 0300-9564 UR - https://m2.mtmt.hu/api/publication/32507645 ID - 32507645 LA - English DB - MTMT ER - TY - CHAP AU - Dobos-Kovács, Mihály AU - Vörös, András ED - Pataki, Béla TI - Model checking and test generation: towards a combined approach to software verification T2 - Proceedings of the 26th Minisymposium of the Department of Measurement and Information Systems PB - BME Méréstechnika és Információs Rendszerek Tanszék CY - Budapest SN - 9789633133149 PY - 2019 SP - 12 EP - 15 PG - 4 UR - https://m2.mtmt.hu/api/publication/31396950 ID - 31396950 LA - English DB - MTMT ER -