2025S

• Bachelor Thesis / 184.695 / PR
• Doctoral & Master Students Seminar / 181.224 / SE
• SAT Solving / 184.090 / VU

• Incremental SAT and SMT Reasoning for Scalable Verification
  2021 – 2024 / Austrian Science Fund (FWF)
  Publications: 189828 / 193053 / 211103 / 211102 / 209320 / 209852 / 209835 / 210159

• Satisfiability Modulo User Propagators / Fazekas, K., Niemetz, A., Preiner, M., Kirchweger, M., Szeider, S., & Biere, A. (2024). Satisfiability Modulo User Propagators. Journal of Artificial Intelligence Research, 81, 989–1017. https://doi.org/10.1613/jair.1.16163
  Projects: INCR (2021–2024) / REVEAL-AI (2020–2024) / SLIM (2019–2024)
• SAT modulo IPASIR-UP / Fazekas, K. (2024, October 14). SAT modulo IPASIR-UP [Presentation]. Dagstuhl Seminar 24421: SAT and Interactions, Wadern, Germany.
  Project: INCR (2021–2024)
• Clausal Equivalence Sweeping / Biere, A., Fazekas, K., Fleury, M., & Froleyks, N. (2024). Clausal Equivalence Sweeping. In N. Narodytska & P. Rümmer (Eds.), Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 (pp. 236–241). TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_29
  Download: Clausal Equivalence Sweeping (688 KB)
• Clausal Congruence Closure / Biere, A., Fazekas, K., Fleury, M., & Froleyks, N. (2024). Clausal Congruence Closure. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024), Pune, India. https://doi.org/10.4230/LIPIcs.SAT.2024.6
  Project: INCR (2021–2024)
• Certifying Incremental SAT Solving / Fazekas, K., Pollitt, F., Fleury, M., & Biere, A. (2024, July 23). Certifying Incremental SAT Solving [Conference Presentation]. 22nd International Workshop on Satisfiability Modulo Theories (SMT 2024), Montreal, Canada. http://hdl.handle.net/20.500.12708/210159
  Project: INCR (2021–2024)
• Incremental SAT Solvers in Practice / Fazekas, K. (2024, June 26). Incremental SAT Solvers in Practice [Conference Presentation]. SAT/SMT/AR Summer School 2024, Nancy, France.
  Project: INCR (2021–2024)
• Incremental Proofs for Bounded Model Checking / Fazekas, K., Pollitt, F., Fleury, M., & Biere, A. (2024). Incremental Proofs for Bounded Model Checking. In MBMV 2024 : 27. Workshop (pp. 133–143). http://hdl.handle.net/20.500.12708/211103
  Project: INCR (2021–2024)
• Certifying Incremental SAT Solving / Fazekas, K., Pollitt, F., Fleury, M., & Biere, A. (2024). Certifying Incremental SAT Solving. In Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning (pp. 321–340). https://doi.org/10.29007/pdcc
  Project: INCR (2021–2024)
• CaDiCaL 2.0 / Biere, A., Faller, T., Fazekas, K., Fleury, M., Froleyks, N., & Pollitt, F. (2024). CaDiCaL 2.0. In Computer Aided Verification (pp. 133–152). Springer. https://doi.org/10.1007/978-3-031-65627-9_7
  Project: INCR (2021–2024)
• SAT-Based Quantified Symmetric Minimization of the Reachable States of Distributed Protocols / Fazekas, K., Aman, G., & Sakallah, K. (2023). SAT-Based Quantified Symmetric Minimization of the Reachable States of Distributed Protocols. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 152–161). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_23
  Download: PDF (499 KB)
• On Incremental Pre-processing for SMT / Bjørner, N., & Fazekas, K. (2023). On Incremental Pre-processing for SMT. In B. Pientka & C. Tinelli (Eds.), Automated Deduction – CADE 29  29th International Conference on Automated Deduction, Rome, Italy, July 1–4, 2023, Proceedings (pp. 41–60). Springer. https://doi.org/10.1007/978-3-031-38499-8_3
  Project: INCR (2021–2024)
• IPASIR-UP: User Propagators for CDCL / Fazekas, K., Niemetz, A., Preiner, M., Kirchweger, M., Szeider, S., & Biere, A. (2023). IPASIR-UP: User Propagators for CDCL. In M. Mahajan & F. Slivovsky (Eds.), 26th International Conference on Theory and Applications of Satisfiability Testing (pp. 8:1-8:13). Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.SAT.2023.8
  Download: PDF (797 KB)
  Projects: INCR (2021–2024) / REVEAL-AI (2020–2024) / SLIM (2019–2024)
• Model Checking AUTOSAR Components with CBMC / Durand, T., Fazekas, K., Weissenbacher, G., & Zwirchmayr, J. (2021). Model Checking AUTOSAR Components with CBMC. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 96–101). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_18
  Download: PDF (206 KB)