Automated Instantiation of Control Flow Tracing Exercises. - Clemens Eisenhofer; Martin Riener (ThEdu@CADE, 2021)

Lemmaless Induction in Trace Logic. - Ahmed Bhayat; Pamina Georgiou; Clemens Eisenhofer; Laura Kovács; Giles Reger (CICM, 2022)

User-Propagators for Custom Theories in SMT Solving. - Nikolaj S. Bjørner; Clemens Eisenhofer; Laura Kovács (SMT, 2022)

Embedding the Connection Calculus in Satisfiability Modulo Theories. - Clemens Eisenhofer; Laura Kovács; Michael Rawson 001 (AReCCa@TABLEAUX, 2023)

Non-Classical Logics in Satisfiability Modulo Theories. - Clemens Eisenhofer; Ruba Alassaf; Michael Rawson 001; Laura Kovács (TABLEAUX, 2023)

Satisfiability Modulo Custom Theories in Z3. - Nikolaj S. Bjørner; Clemens Eisenhofer; Laura Kovács (VMCAI, 2023)

Strongly Analytic Calculi for KLM Logics with SMT-Based Prover. - Agata Ciabattoni; Clemens Eisenhofer; Dmitry Rozplokhas (KR, 2024)

PolySAT: Word-level Bit-vector Reasoning in Z3. - Jakob Rath; Clemens Eisenhofer; Daniela Kaufmann; Nikolaj S. Bjørner; Laura Kovács (VSTTE, 2024)

Spanning Matrices via Satisfiability Solving. - Clemens Eisenhofer; Michael Rawson 001; Laura Kovács (CoRR, 2024)