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
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
International Conference on Computer Aided Verification
(CAV'24)
[ preprint
bib
source
slides
]
Clausal Equivalence Sweeping
Formal Methods in Computer Aided Design
(FMCAD'24)
[ preprint
bib
source
]
Certifying Incremental SAT Solving
International Conference on Logic for Programming, Artificial Intelligence and Reasoning
(LPAR'24)
[ preprint
bib
source
slides
]
Clausal Congruence Closure
International Conference on Theory and Applications of Satisfiability Testing
(SAT'24)
[ preprint
bib
]
Incremental Proofs for Bounded Model Checking
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
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
International Conference on Automated Deduction
(CADE'23)
[ preprint
bib
]
SAT-Based Quantified Symmetric Minimization of the Reachable States of Distributed Protocols
Formal Methods in Computer Aided Design
(FMCAD'23)
[ preprint
bib
source
]
Model Checking AUTOSAR Components with CBMC
Formal Methods in Computer Aided Design
(FMCAD'21)
[ preprint
bib
]
Duplex Encoding of Staircase At-Most-One Constraints for the Antibandwidth Problem
International Conference on the Integration of Constraint Programming, Artificial Intelligence, and Operations Research
(CPAIOR'20)
[ preprint
bib
experiments
slides
talk ]
Incremental Inprocessing SAT Solving
International Conference on Theory and Applications of Satisfiability Testing
(SAT'19)
[ preprint
bib
experiments
slides ]
Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories
International Joint Conference on Automated Reasoning
(IJCAR'18)
[ preprint
bib
experiments
slides ]
Skolem Function Continuation for Quantified Boolean Formulas
International Conference on Tests and Proofs
(TAP'17)
[ preprint
bib
slides ]
A Duality-Aware Calculus for Quantified Boolean Formulas
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
SAT Competition 2020 - Solver and Benchmark Descriptions
(SAT-COMP'20)
[ pdf
bib ]
CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling Entering the SAT Competition 2020
SAT Competition 2020 - Solver and Benchmark Descriptions
(SAT-COMP'20)
[ pdf
bib ]
Workshop talks
Ranking Robustness under Sub-Sampling for the SAT Competition 2018
Pragmatics of SAT
(POS'19)
[ slides ]
Theses