| Publication | Date of Publication | Type |
|---|
| Algorithms for testing membership in univariate quadratic modules over the reals | 2025-01-17 | Paper |
| A new algorithm for Gröbner bases conversion | 2024-12-09 | Paper |
| Interpolation Results for Arrays with Length and MaxDiff | 2023-11-03 | Paper |
| Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties | 2023-08-26 | Paper |
| https://portal.mardi4nfdi.de/entity/Q6159930 | 2023-06-23 | Paper |
| Existence and Construction of a Gr\"obner Basis for a Polynomial Ideal | 2023-06-15 | Paper |
| Consider only general superpositions in completion procedures | 2022-12-09 | Paper |
| Deciding the word problem for ground identities with commutative and extensional symbols | 2022-11-09 | Paper |
| Deciding the word problem for ground and strongly shallow identities w.r.t. extensional symbols | 2022-10-24 | Paper |
| Automated reasoning about parallel algorithms using powerlists | 2022-08-16 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5094130 | 2022-08-02 | Paper |
| Interpolation and amalgamation for arrays with MaxDiff | 2021-10-18 | Paper |
| Algorithms for computing greatest common divisors of parametric multivariate polynomials | 2020-09-19 | Paper |
| An Efficient Algorithm for Computing Parametric Multivariate Polynomial GCD | 2020-09-09 | Paper |
| Connecting Program Synthesis and Reachability: Automatic Program Repair Using Test-Input Generation | 2020-08-05 | Paper |
| NIL: learning nonlinear interpolants | 2020-03-10 | Paper |
| Conditional congruence closure over uninterpreted and interpreted symbols | 2019-03-06 | Paper |
| Lemma discovery in automating induction | 2019-01-15 | Paper |
| The Generalized Rabinowitsch Trick | 2018-04-05 | Paper |
| Shostak's congruence closure as completion | 2017-11-17 | Paper |
| A total, ground path ordering for proving termination of AC-rewrite systems | 2017-11-17 | Paper |
| Comprehensive Gröbner basis theory for a parametric polynomial ideal and the associated completion algorithm | 2017-09-06 | Paper |
| Unification and Matching in Hierarchical Combinations of Syntactic Theories | 2017-02-27 | Paper |
| Conditions for determinantal formula for resultant of a polynomial system | 2017-02-03 | Paper |
| Maximal extensions of simplification orderings | 2017-01-19 | Paper |
| Unification over distributive exponentiation (sub)theories | 2016-09-29 | Paper |
| An algorithm to check whether a basis of a parametric polynomial system is a comprehensive Gröbner basis and the associated completion algorithm | 2016-09-29 | Paper |
| Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF | 2016-09-05 | Paper |
| Conditions for exact resultants using the Dixon formulation | 2015-11-26 | Paper |
| A new algorithm for computing comprehensive Gröbner systems | 2015-09-17 | Paper |
| When Is a Formula a Loop Invariant? | 2015-09-14 | Paper |
| Computing comprehensive Gröbner systems and comprehensive Gröbner bases simultaneously | 2015-06-09 | Paper |
| Operational Termination of Conditional Rewriting with Built-in Numbers and Semantic Data Structures | 2014-07-22 | Paper |
| On Asymmetric Unification and the Combination Problem in Disjoint Theories | 2014-04-16 | Paper |
| On invariant checking | 2014-01-27 | Paper |
| Synthesizing Switching Controllers for Hybrid Systems by Generating Invariants | 2013-08-16 | Paper |
| Hierarchical Combination | 2013-06-14 | Paper |
| Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis | 2013-06-14 | Paper |
| Harald Ganzinger’s Legacy: Contributions to Logics and Programming | 2013-04-19 | Paper |
| Elimination Techniques for Program Analysis | 2013-04-19 | Paper |
| Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants | 2013-04-16 | Paper |
| An efficient method for computing comprehensive Gröbner bases | 2013-03-11 | Paper |
| An efficient algorithm for computing a comprehensive Gröbner system of a parametric polynomial system | 2013-01-10 | Paper |
| A “Hybrid” Approach for Synthesizing Optimal Controllers of Hybrid Systems: A Case Study of the Oil Pump Industrial Example | 2012-11-08 | Paper |
| Rewriting Induction + Linear Arithmetic = Decision Procedure | 2012-09-05 | Paper |
| Program Analysis Using Quantifier-Elimination Heuristics | 2012-07-16 | Paper |
| A brief introduction to Wen-Tsun Wu's Academic career | 2012-05-07 | Paper |
| Termination Analysis of C Programs Using Compiler Intermediate Languages | 2012-04-24 | Paper |
| Multivariate Resultants in Bernstein Basis | 2011-05-26 | Paper |
| An algorithm for computing a Gröbner basis of a polynomial ideal over a ring with zero divisors | 2011-02-19 | Paper |
| Coverset Induction with Partiality and Subsorts: A Powerlist Case Study | 2010-09-14 | Paper |
| Predicting Failures of and Repairing Inductive Proof Attempts | 2010-06-02 | Paper |
| Automatic Generation of Generalization Lemmas for Proving Properties of Tail-Recursive Definitions | 2010-05-07 | Paper |
| Termination of Context-Sensitive Rewriting with Built-In Numbers and Collection Data Structures | 2010-04-27 | Paper |
| Automated Deduction – CADE-19 | 2010-04-20 | Paper |
| Shape Analysis with Reference Set Relations | 2010-01-14 | Paper |
| Advances in Computing Science – ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation | 2009-08-11 | Paper |
| A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs | 2009-07-28 | Paper |
| Cayley-Dixon projection operator for multi-univariate composed polynomials | 2009-06-11 | Paper |
| Dependency Pairs for Rewriting with Non-free Constructors | 2009-03-06 | Paper |
| Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures | 2008-08-28 | Paper |
| Inductive Decidability Using Implicit Induction | 2008-05-27 | Paper |
| Generating all polynomial invariants in simple loops | 2007-10-23 | Paper |
| Bruno Buchberger -- a life devoted to symbolic computation (Preface to the special issue) | 2007-10-23 | Paper |
| Resultants for unmixed bivariate polynomial systems produced using the Dixon formulation | 2007-08-24 | Paper |
| Constructing Sylvester-type resultant matrices using the Dixon formulation | 2007-08-24 | Paper |
| A quantifier-elimination based heuristic for automatically generating inductive assertions for programs | 2007-05-24 | Paper |
| Automatic generation of polynomial invariants of bounded degree using abstract interpretation | 2007-01-22 | Paper |
| Computer Algebra in Scientific Computing | 2006-07-07 | Paper |
| Obituary: Harald Ganzinger | 2006-01-16 | Paper |
| Mechanizing Mathematical Reasoning | 2006-01-10 | Paper |
| Theoretical Aspects of Computing - ICTAC 2004 | 2005-11-30 | Paper |
| Static Analysis | 2005-08-24 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3021913 | 2005-06-21 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4660683 | 2005-04-04 | Paper |
| Automatic Generation of Polynomial Loop Invariants | 2005-03-14 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4657307 | 2005-03-14 | Paper |
| Exact resultants for corner-cut unmixed multivariate polynomial systems using the Dixon formulation | 2004-08-20 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4737127 | 2004-08-11 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4470525 | 2004-07-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4447232 | 2004-02-16 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4539635 | 2002-07-10 | Paper |
| A refinement-based approach to deriving train controllers | 2002-04-11 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2778873 | 2002-03-21 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2738486 | 2002-03-13 | Paper |
| On the construction of a domain language for a class of reactive systems | 2002-02-27 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4234291 | 2001-07-16 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2723430 | 2001-07-05 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4503901 | 2000-09-14 | Paper |
| Using an induction prover for verifying arithmetic circuits | 2000-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4226953 | 1999-07-14 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4227295 | 1999-07-06 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4228470 | 1999-06-21 | Paper |
| Transformational methodology for proving termination of logic programs | 1998-11-05 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3838770 | 1998-08-13 | Paper |
| Solving Polynomial Systems Using a Branch and Prune Approach | 1997-11-02 | Paper |
| New uses of linear arithmetic in automated theorem proving by induction | 1996-11-04 | Paper |
| A path ordering for proving termination of AC rewrite systems | 1995-05-30 | Paper |
| Complexity of unification problems with associative-commutative operators | 1993-12-20 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4202945 | 1993-09-06 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3976057 | 1992-06-26 | Paper |
| Sufficient-completeness, ground-reducibility and their complexity | 1991-01-01 | Paper |
| Automating inductionless induction using test sets | 1991-01-01 | Paper |
| Semi-unification | 1991-01-01 | Paper |
| On ground-confluence of term rewriting systems | 1990-01-01 | Paper |
| Unnecessary inferences in associative-commutative completion procedures | 1990-01-01 | Paper |
| Inference rules and proof procedures for inequations | 1990-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3033866 | 1989-01-01 | Paper |
| Computing a Gröbner basis of a polynomial ideal over a Euclidean domain | 1988-01-01 | Paper |
| Only prime superpositions need be considered in the Knuth-Bendix completion procedure | 1988-01-01 | Paper |
| Wu's method and its application to perspective viewing | 1988-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3805961 | 1988-01-01 | Paper |
| A refutational approach to geometry theorem proving | 1988-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3789100 | 1988-01-01 | Paper |
| Computability and implementability issues in abstract data types | 1988-01-01 | Paper |
| Problem corner: Proving equivalence of different axiomatizations of free groups | 1988-01-01 | Paper |
| A multi-level geometric reasoning system for vision | 1988-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3819992 | 1988-01-01 | Paper |
| Complexity of matching problems | 1987-01-01 | Paper |
| On sufficient-completeness and related properties of term rewriting systems | 1987-01-01 | Paper |
| Proof by consistency | 1987-01-01 | Paper |
| Matching, unification and complexity | 1987-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3774998 | 1987-01-01 | Paper |
| Using Gröbner bases to reason about geometry problems | 1986-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3785940 | 1986-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3783519 | 1986-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3761697 | 1986-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3703293 | 1985-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3696522 | 1985-01-01 | Paper |
| A finite Thue system with decidable word problem and without equivalent finite canonical system | 1985-01-01 | Paper |
| The Knuth-Bendix Completion Procedure and Thue Systems | 1985-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3683533 | 1985-01-01 | Paper |
| An \(O(| T| ^ 3)\) algorithm for testing the Church-Rosser property of Thue systems | 1985-01-01 | Paper |
| Worst-case choice for the stable marriage problem | 1985-01-01 | Paper |
| The Church-Rosser property and special Thue systems | 1985-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3685174 | 1985-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3677849 | 1984-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3319767 | 1983-01-01 | Paper |
| On Proving Uniform Termination and Restricted Termination of Rewriting Systems | 1983-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3687693 | 1982-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3942387 | 1982-01-01 | Paper |
