Folgen
Gereon Kremer
Gereon Kremer
Bestätigte E-Mail-Adresse bei cs.stanford.edu
Titel
Zitiert von
Zitiert von
Jahr
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
962015
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
692022
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
332021
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
302016
Satisfiability checking: Theory and applications
E Ábrahám, G Kremer
International Conference on Software Engineering and Formal Methods, 9-23, 2016
232016
Fully incremental cylindrical algebraic decomposition
G Kremer, E Ábrahám
Journal of Symbolic Computation 100, 11-37, 2020
222020
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
172016
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
92020
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
82017
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
72017
Modular strategic SMT solving with SMT-RAT
G Kremer, E Ábrahám
Acta Universitatis Sapientiae, Informatica 10 (1), 5-25, 2018
62018
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
52021
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
42021
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
32021
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
32019
Evaluation of equational constraints for CAD in SMT solving
R Haehn, G Kremer, E Ábrahám
Satisfiability Checking and Symbolic Computation, 19-32, 2018
32018
Isolating real roots using adaptable-precision interval arithmetic
G Kremer, E Ábrahám
Master’s thesis. RWTH Aachen University, 2013
32013
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
22022
Das System kann den Vorgang jetzt nicht ausführen. Versuchen Sie es später erneut.
Artikel 1–20