Since October 2021, I am a Hertha Firnberg Fellow (funded by FWF) in the group of Formal Methods in Systems Engineering (FORSYTE) at the Technical University of Vienna (TU Wien). In my current research I focus on improving the incremental reasoning methods of SAT and SMT solvers, and thereby aim to push the boundaries of formal verification techniques. I am interested in the theoretical study and practical improvement of algorithms underlying SAT, QBF and SMT solvers.

Previously I was a Research Fellow at the Simons Institute for the Theory of Computing (UC Berkeley) in the program 'Satisfiability: Theory, Practice, and Beyond', under the mentorship of Karem Sakallah (spring semester 2021). Before that, I was a post-doctoral researcher in the FORSYTE group at TU Wien, focusing on the formal verification of AUTOSAR software components with Georg Weissenbacher.

I obtained my PhD in the doctoral program 'Logical Methods in Computer Science' (LogiCS) funded by FWF, under the supervision of Armin Biere, at the Johannes Kepler University Linz in Austria.

Contact

TU Wien
Formal Methods in Systems Engineering
Institute of Logic and Computation
Favoritenstraße 9–11/192-4
A-1040 Vienna, Austria

Email: k DOT katalin DOT fazekas AT gmail DOT com

Publications

CaDiCaL 2.0
Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, Florian Pollitt
International Conference on Computer Aided Verification (CAV'24)
[ preprint | bib | source ]

Certifying Incremental SAT Solving
Katalin Fazekas, Florian Pollitt, Mathias Fleury, Armin Biere
International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'24)
[ preprint | bib | source | slides ]

Clausal Congruence Closure
Armin Biere, Katalin Fazekas, Mathias Fleury and Nils Froleyks
International Conference on Theory and Applications of Satisfiability Testing (SAT'24)
[ preprint | bib ]

Incremental Proofs for Bounded Model Checking
Katalin Fazekas, Florian Pollitt, Mathias Fleury, Armin Biere
Workshop on Methods and Description Languages for Modelling and Verification of Circuits and Systems (MBMV'24)
[ preprint | bib | source | slides ]

IPASIR-UP: User Propagators for CDCL
Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, Armin Biere
Highlighted paper at the International Conference on Theory and Applications of Satisfiability Testing (SAT'23)
[ preprint | bib | source | experiments | slides ]

On Incremental Pre-processing for SMT
Nikolaj Bjørner, Katalin Fazekas
International Conference on Automated Deduction (CADE'23)
[ preprint | bib ]

SAT-Based Quantified Symmetric Minimization of the Reachable States of Distributed Protocols
Katalin Fazekas, Aman Goel, Karem A. Sakallah
Formal Methods in Computer Aided Design (FMCAD'23)
[ preprint | bib | source ]

Model Checking AUTOSAR Components with CBMC
Timothee Durand, Katalin Fazekas, Georg Weissenbacher, Jakob Zwirchmayr
Formal Methods in Computer Aided Design (FMCAD'21)
[ preprint | bib ]

Duplex Encoding of Staircase At-Most-One Constraints for the Antibandwidth Problem
Katalin Fazekas, Markus Sinnl, Armin Biere, Sophie Parragh
International Conference on the Integration of Constraint Programming, Artificial Intelligence, and Operations Research (CPAIOR'20)
[ preprint | bib | experiments | slides | talk ]

Incremental Inprocessing SAT Solving
Katalin Fazekas, Armin Biere, Christoph Scholl
International Conference on Theory and Applications of Satisfiability Testing (SAT'19)
[ preprint | bib | experiments | slides ]

Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories
Katalin Fazekas, Fahiem Bacchus, Armin Biere
International Joint Conference on Automated Reasoning (IJCAR'18)
[ preprint | bib | experiments | slides ]

Skolem Function Continuation for Quantified Boolean Formulas
Katalin Fazekas, Marijn J. H. Heule, Martina Seidl, Armin Biere
International Conference on Tests and Proofs (TAP'17)
[ preprint | bib | slides ]

A Duality-Aware Calculus for Quantified Boolean Formulas
Katalin Fazekas, Martina Seidl, Armin Biere
International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'16)
[ preprint | bib | slides ]

Technical Reports

Duplex Encoding of Antibandwidth Feasibility Formulas Submitted to the SAT Competition 2020
Katalin Fazekas, Markus Sinnl, Armin Biere, Sophie Parragh
SAT Competition 2020 - Solver and Benchmark Descriptions (SAT-COMP'20)
[ pdf | bib ]

CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling Entering the SAT Competition 2020
Armin Biere, Katalin Fazekas, Mathias Fleury, Maximillian Heisinger
SAT Competition 2020 - Solver and Benchmark Descriptions (SAT-COMP'20)
[ pdf | bib ]

Workshop talks

Ranking Robustness under Sub-Sampling for the SAT Competition 2018
Katalin Fazekas, Daniela Kaufmann, Armin Biere
Pragmatics of SAT (POS'19)
[ slides ]

Theses

On SAT-based Solution Methods for Computational Problems
Katalin Fazekas
Dissertation, Johannes Kepler University Linz (JKU)
[ pdf | bib ]

EUF-Proofs for SMT4J
Katalin Fazekas
Master Thesis, Johannes Kepler University Linz (JKU)
[ pdf ]