SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving F Corzilius, G Kremer, S Junges, S Schupp, E Ábrahám International Conference on Theory and Applications of Satisfiability …, 2015 | 96 | 2015 |
cvc5: A Versatile and Industrial-Strength SMT Solver H Barbosa, C Barrett, M Brain, G Kremer, H Lachnitt, M Mann, ... International Conference on Tools and Algorithms for the Construction and …, 2022 | 69 | 2022 |
Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings E Ábrahám, JH Davenport, M England, G Kremer Journal of Logical and Algebraic Methods in Programming 119, 100633, 2021 | 33 | 2021 |
Zephyrus2: On the Fly deployment optimization using SMT and CP technologies E Ábrahám, F Corzilius, EB Johnsen, G Kremer, J Mauro International Symposium on Dependable Software Engineering: Theories, Tools …, 2016 | 30 | 2016 |
Satisfiability checking: Theory and applications E Ábrahám, G Kremer International Conference on Software Engineering and Formal Methods, 9-23, 2016 | 23 | 2016 |
Fully incremental cylindrical algebraic decomposition G Kremer, E Ábrahám Journal of Symbolic Computation 100, 11-37, 2020 | 22 | 2020 |
A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic G Kremer, F Corzilius, E Ábrahám International Workshop on Computer Algebra in Scientific Computing, 315-335, 2016 | 17 | 2016 |
New Opportunities for the Formal Proof of Computational Real Geometry? E Ábrahám, J Davenport, M England, G Kremer, Z Tonks Proceedings of the 5th Workshop on Satisfiability Checking and Symbolic …, 2020 | 13* | 2020 |
Cylindrical Algebraic Decomposition for Nonlinear Arithmetic Problems G Kremer PhD dissertation, RWTH Aachen University, 2020 | 9 | 2020 |
Embedding the Virtual Substitution Method in the Model Constructing Satisfiability Calculus Framework. E Ábrahám, J Nalbach, G Kremer SC²@ ISSAC, 2017 | 9* | 2017 |
Comparing Different Projection Operators in the Cylindrical Algebraic Decomposition for SMT Solving. T Viehmann, G Kremer, E Ábrahám SC²@ ISSAC, 2017 | 8 | 2017 |
SMT Solving for Arithmetic Theories: Theory and Tool Support E Ábrahám, G Kremer 2017 19th International Symposium on Symbolic and Numeric Algorithms for …, 2017 | 7 | 2017 |
Modular strategic SMT solving with SMT-RAT G Kremer, E Ábrahám Acta Universitatis Sapientiae, Informatica 10 (1), 5-25, 2018 | 6 | 2018 |
On the Implementation of Cylindrical Algebraic Coverings for Satisfiability Modulo Theories Solving G Kremer, E Ábrahám, M England, JH Davenport 2021 23rd International Symposium on Symbolic and Numeric Algorithms for …, 2021 | 5 | 2021 |
Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic E Abrahám, JH Davenport, M England, G Kremer arXiv preprint arXiv:2108.05320, 2021 | 4 | 2021 |
Implementing arithmetic over algebraic numbers A tutorial for Lazard's lifting scheme in CAD G Kremer, J Brandt 2021 23rd International Symposium on Symbolic and Numeric Algorithms for …, 2021 | 3 | 2021 |
On variable orderings in MCSAT for non-linear real arithmetic J Nalbach, G Kremer, E Ábrahám Satisfiability Checking and Symbolic Computation 2460, 6, 2019 | 3 | 2019 |
Evaluation of equational constraints for CAD in SMT solving R Haehn, G Kremer, E Ábrahám Satisfiability Checking and Symbolic Computation, 19-32, 2018 | 3 | 2018 |
Isolating real roots using adaptable-precision interval arithmetic G Kremer, E Ábrahám Master’s thesis. RWTH Aachen University, 2013 | 3 | 2013 |
Flexible Proof Production in an Industrial-Strength SMT Solver H Barbosa, A Reynolds, G Kremer, H Lachnitt, A Niemetz, A Nötzli, ... Automated Reasoning, 15, 2022 | 2 | 2022 |