My research establishes synergies between computer algebra and automated deduction in support of automated reasoning about software systems. As such, my work

enhances automated deduction with computer algebra insights;
extends computer algebra methods by automated deduction approaches;
designs hybrid approaches complementing computer algebra and automated deduction;
develops software artefacts combining computer algebra and automated deduction.

By developing methods based on a tight interactions between computer algebra and automated reasoning, I promote research on:

algebraic analysis of systems, in particular for invariant synthesis, termination analysis and probabilistic reasoning;
deductive verification, in particular focusing on safety and security verification;
SMT solving, in particular addressing on-demand theory reasoning;
first-order theorem proving, in particular targeting quantified reasoning with theory extensions.