Embedding the Virtual Substitution Method in the Model Constructing Satisfiability Calculus Framework. - Erika Ábrahám; Jasper Nalbach; Gereon Kremer (SC²@ISSAC, 2017)

On Variable Orderings in MCSAT for Non-Linear Real Arithmetic. - Jasper Nalbach; Gereon Kremer; Erika Ábrahám (SC-square@SIAM AG, 2019)

Extending the Fundamental Theorem of Linear Programming for Strict Inequalities. - Jasper Nalbach; Erika Ábrahám; Gereon Kremer (ISSAC, 2021)

Cylindrical Algebraic Coverings for Quantifiers (short paper). - Gereon Kremer; Jasper Nalbach (SC-Square@FLoC, 2022)

Subtropical Satisfiability for SMT Solving. - Jasper Nalbach; Erika Ábrahám (NFM, 2023)

Exploiting Strict Constraints in the Cylindrical Algebraic Covering. - Philipp Bär; Jasper Nalbach; Erika Ábrahám; Christopher W. Brown 001 (SMT, 2023)

Automated Exercise Generation for Satisfiability Checking. - Erika Ábrahám; Jasper Nalbach; Valentin Promies (FMTea, 2023)

FMplex: A Novel Method for Solving Linear Real Arithmetic Problems (Extended Version). - Jasper Nalbach; Valentin Promies; Erika Ábrahám; Paul Kobialka (CoRR, 2023)

FMplex: A Novel Method for Solving Linear Real Arithmetic Problems. - Jasper Nalbach; Valentin Promies; Erika Ábrahám; Paul Kobialka (GandALF, 2023)

Merging Adjacent Cells During Single Cell Construction. - Jasper Nalbach; Erika Ábrahám (CASC, 2024)

Under-Approximation of a Single Algebraic Cell (Extended Abstract). - Valentin Promies; Jasper Nalbach; Erika Ábrahám (PAAR+SC²@IJCAR, 2024)

On Projective Delineability. - Lucas Michel; Jasper Nalbach; Pierre Mathonet; Naïm Zénaïdi; Christopher W. Brown 001; Erika Ábrahám; James H. Davenport; Matthew England 001 (SYNASC, 2024)

Extensions of the Cylindrical Algebraic Covering Method for Quantifiers. - Jasper Nalbach; Gereon Kremer (CoRR, 2024)

Levelwise construction of a single cylindrical algebraic cell. - Jasper Nalbach; Erika Ábrahám; Philippe Specht; Christopher W. Brown 001; James H. Davenport; Matthew England 001 (J. Symb. Comput., 2024)

More is Less: Adding Polynomials for Faster Explanations in NLSAT. - Valentin Promies; Jasper Nalbach; Erika Ábrahám; Paul Wagner (CADE, 2025)

FMplex: Exploring a Bridge between Fourier-Motzkin and Simplex. - Valentin Promies; Jasper Nalbach; Erika Ábrahám; Paul Kobialka (Log. Methods Comput. Sci., 2025)