@inproceedings{MTMT:36408262,
	title = {Beyond Hello World: Teaching software engineering with realistic and automated assignments},
	url = {https://m2.mtmt.hu/api/publication/36408262},
	author = {Dobos-Kovács, Mihály and Vörös, András and Micskei, Zoltán Imre},
	booktitle = {Proceedings of the International Conference on Formal Methods and Foundations of Artificial Intelligence},
	doi = {10.17048/fmfai.2025.51},
	unique-id = {36408262},
	abstract = {Software engineering is a complex discipline that requires engineers to blend various skills to produce quality software adeptly. In this paper, we propose a software engineering assignment that follows the lifecycle of a feature of a real-world project, mimics real-world challenges, promotes best practices, and shows the importance of verification techniques. We deploy the assignment in a university course and discuss our findings regarding functional correctness, code quality, and being on schedule. Finally, we propose an AI-assisted outcome estimation method to help identify struggling students while the home assignment is ongoing.},
	year = {2025},
	pages = {51-64},
	orcid-numbers = {Dobos-Kovács, Mihály/0000-0002-0064-2965; Micskei, Zoltán Imre/0000-0003-1846-261X}
}

@article{MTMT:36429902,
	title = {CHCVerif: A Portfolio-Based Solver for Constrained Horn Clauses},
	url = {https://m2.mtmt.hu/api/publication/36429902},
	author = {Dobos-Kovács, Mihály and Bajczi, Levente and Vörös, András},
	doi = {10.4204/EPTCS.434.6},
	journal-iso = {ELECTRON PROC THEOR COMPUT SCI},
	journal = {ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE},
	volume = {434},
	unique-id = {36429902},
	abstract = {Constrained Horn Clauses (CHCs) are widely adopted as intermediate representations for a variety of verification tasks, including safety checking, invariant synthesis, and inter procedural analysis. This paper introduces CHCVERIF, a portfolio-based CHC solver that adopts a software verification approach for solving CHCs. This approach enables us to reuse mature software verification tools to tackle CHC benchmarks, particularly those involving bitvectors and low-level semantics. Our evaluation shows that while the method enjoys only moderate success with linear integer arithmetic, it achieves modest success on bitvector benchmarks. Moreover, our results demonstrate the viability and potential of using software verification tools as backends for CHC solving, particularly when supported by a carefully constructed portfolio. © Dobos-Kovács et al.},
	year = {2025},
	eissn = {2075-2180},
	pages = {40-51},
	orcid-numbers = {Dobos-Kovács, Mihály/0000-0002-0064-2965; Bajczi, Levente/0000-0002-6551-5860}
}

@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: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: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:33575796,
	title = {Evaluation of SMT solvers in abstraction-based software model checking},
	url = {https://m2.mtmt.hu/api/publication/33575796},
	author = {Dobos-Kovács, Mihály and Vörös, András},
	booktitle = {Proceedings of the 11th Latin-American Symposium on Dependable Computing, LADC '22},
	doi = {10.1145/3569902.3570187},
	unique-id = {33575796},
	year = {2022},
	pages = {109-116},
	orcid-numbers = {Dobos-Kovács, Mihály/0000-0002-0064-2965}
}

@CONFERENCE{MTMT:32131082,
	title = {Median raphe region serotoninergic neurones affect depressive-like behaviour and vegetative functions, but not social behaviour},
	url = {https://m2.mtmt.hu/api/publication/32131082},
	author = {Csilla, Lea Fazekas and Manon, Bellardie and Bibiána, Török and Eszter, Sipos and Dobos-Kovács, Mihály and Elodie, Chaillou and Zelena, Dóra},
	booktitle = {Medical Conference for PhD Students and Experts of Clinical Sciences 2021},
	unique-id = {32131082},
	year = {2021},
	pages = {108-108},
	orcid-numbers = {Dobos-Kovács, Mihály/0000-0002-0064-2965}
}

@inproceedings{MTMT:32678888,
	title = {Bitvector Support in the Theta Formal Verification Framework},
	url = {https://m2.mtmt.hu/api/publication/32678888},
	author = {Dobos-Kovács, Mihály and Hajdu, Ákos and Vörös, András},
	booktitle = {2021 10th Latin-American Symposium on Dependable Computing (LADC)},
	doi = {10.1109/LADC53747.2021.9672595},
	unique-id = {32678888},
	year = {2021},
	pages = {01-08},
	orcid-numbers = {Dobos-Kovács, Mihály/0000-0002-0064-2965; Hajdu, Ákos/0000-0001-8001-8865}
}

@article{MTMT:32399092,
	title = {Pharmacogenetic excitation of the median raphe region affects social and depressive-like behavior and core body temperature in male mice},
	url = {https://m2.mtmt.hu/api/publication/32399092},
	author = {Fazekas, Csilla Lea and Bellardie, M and Szocsics-Török, Bibiána and Bodóné Sipos, Eszter and Tóth, Blanka and Baranyi, Mária and Sperlágh, Beáta and Dobos-Kovács, Mihály and Chaillou, E and Zelena, Dóra},
	doi = {10.1016/j.lfs.2021.120037},
	journal-iso = {LIFE SCI},
	journal = {LIFE SCIENCES},
	volume = {286},
	unique-id = {32399092},
	issn = {0024-3205},
	year = {2021},
	eissn = {1879-0631},
	orcid-numbers = {Dobos-Kovács, Mihály/0000-0002-0064-2965}
}