Since May 2023, I am a postdoctoral researcher at the Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany, advised by Prof. Dr. Rupak Majumdar.

Research Interests

My research work focuses on automatically ensuring and increasing the correctness (i.e., soundness and completeness/precision), consistency, and performance of various types of software systems, from program analysis tools (such as static analyzers, SMT solvers, and deductive verifiers) to distributed systems and large language models (LLMs).

Student Projects

I am happy to advise students for their Bachelor or Master theses, practical work, or internships. Some example projects that I currently have available are:

• Refactoring-based Benchmarks Generation
• Model Fuzzing: Testing Probabilistic Model Checkers via Mutation-based Fuzzing

If the project you would like to work on is not in this list, please contact me and we will try to find together a suitable topic.

Education

• PhD in Computer Science: ETH Zürich, Switzerland, 2016 - 2022
  • Dissertation: Automatically Identifying Soundness and Completeness Errors in Program Analysis Tools
  • Advisor: Prof. Dr. Peter Müller
• MSc. in Computer Science (European Master in Software Engineering): Free University of Bozen-Bolzano, Italy and Technische Universität Kaiserslautern, Germany, 2013 - 2015
  • Thesis: Alternative Approaches for Quantitative State/Event Fault Trees Analysis
  • Advisors: Prof. Dr. Barbara Russo, Prof. Dr. Peter Liggesmeyer, MSc. Michael Roth
• BSc. in Computer and Software Engineering (Major in Software Engineering): Politehnica University of Timisoara, Romania, 2009 - 2013
  • Thesis: Extensions of the phantm Analyzer to support Model Extraction from PHP Web Applications
  • Advisor: Prof. Dr. Marius Minea

Publications

• Identifying Overly Restrictive Matching Patterns in SMT-based Program Verifiers (extended version), A. Bugariu, A. Ter-Gabrielyan, P. Müller, Formal Aspects of Computing (FAC), 2023
• Identifying Overly Restrictive Matching Patterns in SMT-based Program Verifiers, A. Bugariu, A. Ter-Gabrielyan, P. Müller, Formal Methods (FM), 2021
• Automatically Testing String Solvers, A. Bugariu, P. Müller, Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering (ICSE), 2020
• Automatically Testing Implementations of Numerical Abstract Domains, A. Bugariu, V. Wüstholz, M. Christakis, P. Müller, Automated Software Engineering (ASE), 2018

Service

• SOAP’24, OOPSLA’24, ICSE’24 AEC, ECOOP’23 ERC, ECOOP’23 AEC, Fuzzing’22 AEC, PLDI’22 AEC, CAV’21 AEC, PLDI’21 AEC: PC member
• STTT’25, TOSEM’22 Replicated Computational Results: Reviewer
• ETH Zürich Hiring Committee for Computer Science’21: Scientific staff representative
• PLDI’19, ECOOP/PLDI’17: Student volunteer

Teaching

• Rigorous Software Engineering, BSc. course, ETH Zürich: Invited lecturer (SS’24), Co-lecturer (SS’23), Teaching assistant (SS’20)
• Concepts of Object-Oriented Programming, MSc. course, ETH Zürich: Head teaching assistant (AS’21, AS’20), Teaching assistant (AS’19, AS’18, AS’17)
• Parallel Programming, BSc. course, ETH Zürich: Teaching assistant (SS’19)
• Research Topics in Software Engineering, MSc. seminar, ETH Zürich: Teaching assistant (AS’19, AS’17)
• Software Architecture and Engineering, BSc. course, ETH Zürich: Head teaching assistant (SS’18), Teaching assistant (SS’17)
• Informatik I, BSc. course, ETH Zürich: Teaching assistant (AS’16)

Advised Students

• H. Mehmood: Automatically Checking LLM-Generated Answers, MSc. Thesis, University of Kaiserslautern-Landau (AS’24)
• S. Kühne: Automatically Explaining and Localizing Semantic Errors in SMT Solvers, MSc. Thesis, ETH Zürich (AS’24)
• R. van Doren: Alternative SMT Encodings for Congestion Control Algorithms, Practical Work, ETH Zürich (SS’24)
• S. Kühne: Automatically Testing Solvers for String and Regular Expressions Constraints, BSc. Thesis, ETH Zürich (AS’21)
• K. Thommen: Automatically Testing MAX-SMT Solvers, BSc. Thesis, ETH Zürich (AS’21)
• M. Hurmuz: Automatically Generating Java Benchmarks with Known Errors, MSc. Thesis, ETH Zürich (AS’21)
• O. Becker: Automatically Testing SMT Solvers, BSc. Thesis, ETH Zürich (AS’21)
• P. Strebel: Explaining Unsatisfiability Proofs through Examples, BSc. Thesis, ETH Zürich (SS’21) (co-advised with Dr. Malte Schwerhoff)
• R. Sherif Abdelbar: Automated Checking of Implicit Assumptions on Textual Data, BSc. Thesis, ETH Zürich (SS’18) (co-advised with Dr. Caterina Urban)
• M. Schumacher: Automated Generation of Data Quality Checks, MSc. Thesis, ETH Zürich (AS’17) (co-advised with Dr. Caterina Urban)