About Me

I am a PhD student at the Budapest University of Technology and Economics, working on formal methods, mainly model checkers. I am interested in the model checking process, as a whole: from different application domains and model transformations through different algorithms, portfolios and algorithm selection to validation and certification. My focus is on applicability and usability of model checkers on real world projects. I have experience not just with software verification, but also with the formal verification of PLC code, hardware and engineering models.

My PhD advisor is Dr. Zoltán Micskei.

Education

2023 - present: Budapest University of Technology and Economics Computer science PhD, advised by Dr. Zoltán Micskei
2022 - 2023: Budapest University of Technology and Economics Computer Engineering MSc thesis
2018 - 2022: Budapest University of Technology and Economics Computer Engineering BSc thesis

Internships, Experience

2023, 2024 Summer: LMU, Munich, Germany, Research Stay I spent two months working on validation of correctness proofs of hardware and software modelcheckers at the Software Systems Laboratory under the supervision of Prof. Dr. Dirk Beyer, Nian-Ze Lee and Po-Chun Chien.
2022 Summer: CERN, Meyrin, CERN Summer Student I learned about and worked on PLC verification, mainly requirement formalization as part of the Industrial Control Systems Group in the Beam Department for two months.
2021 - 2022: thyssenkrupp, Budapest, Hungary, Software Engineering Intern Developing rules for C verification with static analyzer based on the in-house coding guidelines

Volunteering

2017 - 2019: Skool, Budapest, Hungary, Mentor & Programming Tutor Helping young girls start their journey with programming and computer science.
2023 - 2024: Girl’s STEM Day, Budapest, HU, Presenter I was a presenter at the university faculty’s open lab program.
2017, 2018, 2024: Researcher’s Night, Budapest, Hungary, Presenter at Demos I presented demos at the demonstration organized by my research group (ftsrg) at the university.

Tools

2020 - present: Theta Generic, modular and configurable model checking framework.
2023 - present: Btor2Cert A Certifying and Validating Hardware-Verification Framework Using Software Analyzers.
2022: PLCverif integration with FRET Integrating FRET, a framework for the specification and formalization of requirements into PLCverif, a formal verification tool for PLC programs.