2025S

• Logic and Reasoning in Computer Science / 192.033 / VU
• Project in Computer Science 2 Trends in cloud computing / 192.035 / PR

• PolySAT: Word-level Bit-vector Reasoning in Z3 / Rath, J., Eisenhofer, C., Kaufmann, D., Bjørner, N., & Kovacs, L. (2024, October 14). PolySAT: Word-level Bit-vector Reasoning in Z3 [Conference Presentation]. VSTTE 2024, Prague, Czechia. http://hdl.handle.net/20.500.12708/211021
  Projects: ARTIST (2021–2026) / SFB SPyCoDe (2023–2026)
• Strongly Analytic Calculi for KLM Logics with SMT-Based Prover / Ciabattoni, A., Eisenhofer, C., & Rozplokhas, D. (2024). Strongly Analytic Calculi for KLM Logics with SMT-Based Prover. In Proceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning (pp. 284–294). https://doi.org/10.24963/kr.2024/27
  Project: TAIGER (2023–2027)
• Embedding the Connection Calculus in Satisfiability Modulo Theories / Eisenhofer, C., Kovács, L., & Rawson, M. (2024). Embedding the Connection Calculus in Satisfiability Modulo Theories. In Proceedings of the 1st International Workshop on Automated Reasoning with Connection Calculi (AReCCa 2023) (pp. 54–63). CEUR-WS.org. https://doi.org/10.34726/5394
  Download: PDF (248 KB)
  Projects: ARTIST (2021–2026) / ForSmart (2023–2027) / SFB SPyCoDe (2023–2026)
• Non-Classical Logics in Satisfiability Modulo Theories / Eisenhofer, C., Alassaf, R., Rawson, M., & Kovács, L. (2023). Non-Classical Logics in Satisfiability Modulo Theories. In D. R. S. Ramanayake & J. Urban (Eds.), Automated Reasoning with Analytic Tableaux and Related Methods: 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings (pp. 24–36). Springer. https://doi.org/10.1007/978-3-031-43513-3_2
  Download: PDF (423 KB)
  Projects: ARTIST (2021–2026) / SFB SPyCoDe (2023–2026)
• Satisfiability Modulo Custom Theories in Z3 / Bjørner, N., Eisenhofer, C., & Kovács, L. (2023). Satisfiability Modulo Custom Theories in Z3. In C. Dragoi, M. Emmi, & J. Wang (Eds.), Verification, Model Checking, and Abstract Interpretation. VMCAI 2023 (pp. 91–105). Springer. https://doi.org/10.1007/978-3-031-24950-1_5
  Project: ARTIST (2021–2026)
• User-Propagation for Custom Theories in SMT Solving / Eisenhofer, C. (2022, September 14). User-Propagation for Custom Theories in SMT Solving [Presentation]. 14th Alpine Verification Meeting, Frauenchiemsee, Germany. http://hdl.handle.net/20.500.12708/154343
  Project: ARTIST (2021–2026)
• User-Propagation for Custom Theories in SMT Solving / Bjorner, N., Eisenhofer, C., & Kovács, L. (2022). User-Propagation for Custom Theories in SMT Solving. In D. Deharbe & A. Hyvärinen (Eds.), Satisfiability Modulo Theories. 20th International Workshop. SMT 2022. Proceedings (pp. 71–79). CEUR-WS.org. https://doi.org/10.34726/4104
  Download: PDF (1.15 MB)
  Project: ARTIST (2021–2026)
• Automated Instantiation of Control Flow Tracing Exercises / Eisenhofer, C., & Riener, M. (2022). Automated Instantiation of Control Flow Tracing Exercises. In J. Marcos, W. Neuper, & P. Quaresma (Eds.), Proceedings 10th International Workshop on Theorem Proving Components for Educational Software (pp. 43–58). EPTCS. https://doi.org/10.4204/EPTCS.354.4
  Download: PDF (629 KB)
• Lemmaless Induction in Trace Logic / Bhayat, A., Georgiou, P., Eisenhofer, C., Kovács, L., & Reger, G. (2022). Lemmaless Induction in Trace Logic. In K. Buzzard & T. Kutsia (Eds.), Intelligent Computer Mathematics : 15th International Conference, CICM 2022, Tbilisi, Georgia, September 19–23, 2022, Proceedings (pp. 191–208). https://doi.org/10.34726/5860
  Download: PDF (320 KB)
  Project: DK - Logic (2014–2023)
• User propagators for satisfiability modulo custom theories / Eisenhofer, C. (2022). User propagators for satisfiability modulo custom theories [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2022.100221
  Download: PDF (1.13 MB)