Three-valued automated reasoning on analog properties. - Raffaella Gentilini; Klaus Schneider 001; Alexander Dreyer (ACM Great Lakes Symposium on VLSI, 2007)

Combining Interval Arithmetic and Three-Valued Temporal Logics for the Verification of Analog Systems. - Raffaella Gentilini; Klaus Schneider 001; Alexander Dreyer (MBMV, 2007)

Solving hard instances in QF-BV combining Boolean reasoning with computer algebra. - Markus Wedler; Evgeny Pavlenko; Alexander Dreyer; Frank Seelisch; Dominik Stoffel; Gert-Martin Greuel; Wolfgang Kunz (Algorithms and Applications for Next Generation SAT Solvers, 2009)

PolyBoRi: A framework for Gröbner-basis computations with Boolean polynomials. - Michael Brickenstein; Alexander Dreyer (J. Symb. Comput., 2009)

Network-driven Boolean Normal Forms. - Michael Brickenstein; Alexander Dreyer (Verification over discrete-continuous boundaries, 2010)

Fast and Robust Symbolic Model Order Reduction with Analog Insydes. - Matthias Hauser; Christian Salzig; Alexander Dreyer (CASC, 2011)

STABLE: A new QF-BV SMT Solver for hard Verification Problems combining Boolean Reasoning with Computer Algebra. - Evgeny Pavlenko; Markus Wedler; Dominik Stoffel; Wolfgang Kunz; Alexander Dreyer; Frank Seelisch; Gert-Martin Greuel (MBMV, 2011)

Proof logging for computer algebra based SMT solving. - Oliver Marx; Markus Wedler; Dominik Stoffel; Wolfgang Kunz; Alexander Dreyer (ICCAD, 2013)

Gröbner-free normal forms for Boolean polynomials. - Michael Brickenstein; Alexander Dreyer (J. Symb. Comput., 2013)