| 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
Journal of Symbolic Computation | 2024-12-09 | Paper |
Interpolation Results for Arrays with Length and MaxDiff
ACM Transactions on Computational Logic | 2023-11-03 | Paper |
Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties
Logical Methods in Computer Science | 2023-08-26 | Paper |
| scientific article; zbMATH DE number 7700620 (Why is no real title available?) | 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
Rewriting Techniques and Applications | 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
Journal of Automated Reasoning | 2022-10-24 | Paper |
Automated reasoning about parallel algorithms using powerlists
Algebraic Methodology and Software Technology | 2022-08-16 | Paper |
scientific article; zbMATH DE number 7566058 (Why is no real title available?)
(available as arXiv preprint) | 2022-08-02 | Paper |
| scientific article; zbMATH DE number 7566058 (Why is no real title available?) | 2022-08-02 | Paper |
Interpolation and amalgamation for arrays with MaxDiff
(available as arXiv preprint) | 2021-10-18 | Paper |
Algorithms for computing greatest common divisors of parametric multivariate polynomials
Journal of Symbolic Computation | 2020-09-19 | Paper |
An Efficient Algorithm for Computing Parametric Multivariate Polynomial GCD
Proceedings of the 2018 ACM International Symposium on Symbolic and Algebraic Computation | 2020-09-09 | Paper |
Connecting program synthesis and reachability: automatic program repair using test-input generation
Tools and Algorithms for the Construction and Analysis of Systems | 2020-08-05 | Paper |
NIL: learning nonlinear interpolants
(available as arXiv preprint) | 2020-03-10 | Paper |
Conditional congruence closure over uninterpreted and interpreted symbols
Journal of Systems Science and Complexity | 2019-03-06 | Paper |
Lemma discovery in automating induction
Automated Deduction — Cade-13 | 2019-01-15 | Paper |
The generalized Rabinowitsch trick
Applications of Computer Algebra | 2018-04-05 | Paper |
Shostak's congruence closure as completion
Rewriting Techniques and Applications | 2017-11-17 | Paper |
A total, ground path ordering for proving termination of AC-rewrite systems
Rewriting Techniques and Applications | 2017-11-17 | Paper |
Comprehensive Gröbner basis theory for a parametric polynomial ideal and the associated completion algorithm
Journal of Systems Science and Complexity | 2017-09-06 | Paper |
Unification and matching in hierarchical combinations of syntactic theories
Frontiers of Combining Systems | 2017-02-27 | Paper |
Conditions for determinantal formula for resultant of a polynomial system
Proceedings of the 2006 international symposium on Symbolic and algebraic computation | 2017-02-03 | Paper |
Maximal extensions of simplification orderings
Lecture Notes in Computer Science | 2017-01-19 | Paper |
Unification over distributive exponentiation (sub)theories
Journal of Automata, Languages and Combinatorics | 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
Proceedings of the 2015 ACM on International Symposium on Symbolic and Algebraic Computation | 2016-09-29 | Paper |
Interpolant synthesis for quadratic polynomial inequalities and combination with EUF
Automated Reasoning | 2016-09-05 | Paper |
Conditions for exact resultants using the Dixon formulation
Proceedings of the 2000 international symposium on Symbolic and algebraic computation | 2015-11-26 | Paper |
A new algorithm for computing comprehensive Gröbner systems
Proceedings of the 2010 International Symposium on Symbolic and Algebraic Computation | 2015-09-17 | Paper |
When is a formula a loop invariant?
Lecture Notes in Computer Science | 2015-09-14 | Paper |
Computing comprehensive Gröbner systems and comprehensive Gröbner bases simultaneously
Proceedings of the 36th international symposium on Symbolic and algebraic computation | 2015-06-09 | Paper |
Operational termination of conditional rewriting with built-in numbers and semantic data structures
Electronic Notes in Theoretical Computer Science | 2014-07-22 | Paper |
On Asymmetric Unification and the Combination Problem in Disjoint Theories
Lecture Notes in Computer Science | 2014-04-16 | Paper |
On invariant checking
Journal of Systems Science and Complexity | 2014-01-27 | Paper |
Synthesizing switching controllers for hybrid systems by generating invariants
Theories of Programming and Formal Methods | 2013-08-16 | Paper |
Asymmetric unification: a new unification paradigm for cryptographic protocol analysis
Automated Deduction – CADE-24 | 2013-06-14 | Paper |
Hierarchical Combination
Automated Deduction – CADE-24 | 2013-06-14 | Paper |
Harald Ganzinger's legacy: contributions to logics and programming
Programming Logics | 2013-04-19 | Paper |
Elimination Techniques for Program Analysis
Programming Logics | 2013-04-19 | Paper |
Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants
Automated Reasoning and Mathematics | 2013-04-16 | Paper |
An efficient method for computing comprehensive Gröbner bases
Journal of Symbolic Computation | 2013-03-11 | Paper |
An efficient algorithm for computing a comprehensive Gröbner system of a parametric polynomial system
Journal of Symbolic Computation | 2013-01-10 | Paper |
A ``hybrid approach for synthesizing optimal controllers of hybrid systems: a case study of the oil pump industrial example
FM 2012: Formal Methods | 2012-11-08 | Paper |
Rewriting Induction + Linear Arithmetic = Decision Procedure
Automated Reasoning | 2012-09-05 | Paper |
Program analysis using quantifier-elimination heuristics (extended abstract)
Lecture Notes in Computer Science | 2012-07-16 | Paper |
A brief introduction to Wen-Tsun Wu's Academic career
Journal of Symbolic Computation | 2012-05-07 | Paper |
| Termination Analysis of C Programs Using Compiler Intermediate Languages | 2012-04-24 | Paper |
Multivariate resultants in Bernstein basis
Automated Deduction in Geometry | 2011-05-26 | Paper |
An algorithm for computing a Gröbner basis of a polynomial ideal over a ring with zero divisors
Mathematics in Computer Science | 2011-02-19 | Paper |
Coverset induction with partiality and subsorts: a powerlist case study
Interactive Theorem Proving | 2010-09-14 | Paper |
Predicting failures of and repairing inductive proof attempts
Next Generation Design and Verification Methodologies for Distributed Embedded Control Systems | 2010-06-02 | Paper |
Automatic generation of generalization lemmas for proving properties of tail-recursive definitions
Lecture Notes in Computer Science | 2010-05-07 | Paper |
Termination of Context-Sensitive Rewriting with Built-In Numbers and Collection Data Structures
Functional and Constraint Logic Programming | 2010-04-27 | Paper |
Deciding inductive validity of equations.
Lecture Notes in Computer Science | 2010-04-20 | Paper |
Shape analysis with reference set relations
Lecture Notes in Computer Science | 2010-01-14 | Paper |
Advances in Computing Science – ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation
Lecture Notes in Computer Science | 2009-08-11 | Paper |
A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs
Automated Deduction – CADE-22 | 2009-07-28 | Paper |
Cayley-Dixon projection operator for multi-univariate composed polynomials
Journal of Symbolic Computation | 2009-06-11 | Paper |
Dependency Pairs for Rewriting with Non-free Constructors
Automated Deduction – CADE-21 | 2009-03-06 | Paper |
Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures
Rewriting Techniques and Applications | 2008-08-28 | Paper |
Inductive Decidability Using Implicit Induction
Logic for Programming, Artificial Intelligence, and Reasoning | 2008-05-27 | Paper |
Bruno Buchberger -- a life devoted to symbolic computation (Preface to the special issue)
Journal of Symbolic Computation | 2007-10-23 | Paper |
Generating all polynomial invariants in simple loops
Journal of Symbolic Computation | 2007-10-23 | Paper |
Resultants for unmixed bivariate polynomial systems produced using the Dixon formulation
Journal of Symbolic Computation | 2007-08-24 | Paper |
Constructing Sylvester-type resultant matrices using the Dixon formulation
Journal of Symbolic Computation | 2007-08-24 | Paper |
A quantifier-elimination based heuristic for automatically generating inductive assertions for programs
Journal of Systems Science and Complexity | 2007-05-24 | Paper |
Automatic generation of polynomial invariants of bounded degree using abstract interpretation
Science of Computer Programming | 2007-01-22 | Paper |
Computer Algebra in Scientific Computing
Lecture Notes in Computer Science | 2006-07-07 | Paper |
Obituary: Harald Ganzinger
Journal of Automated Reasoning | 2006-01-16 | Paper |
Mechanizing Mathematical Reasoning
Lecture Notes in Computer Science | 2006-01-10 | Paper |
Theoretical Aspects of Computing - ICTAC 2004
Lecture Notes in Computer Science | 2005-11-30 | Paper |
Static Analysis
Lecture Notes in Computer Science | 2005-08-24 | Paper |
| scientific article; zbMATH DE number 2177631 (Why is no real title available?) | 2005-06-21 | Paper |
| scientific article; zbMATH DE number 2151215 (Why is no real title available?) | 2005-04-04 | Paper |
| scientific article; zbMATH DE number 2145003 (Why is no real title available?) | 2005-03-14 | Paper |
Automatic Generation of Polynomial Loop Invariants
Proceedings of the 2004 international symposium on Symbolic and algebraic computation | 2005-03-14 | Paper |
Exact resultants for corner-cut unmixed multivariate polynomial systems using the Dixon formulation
Journal of Symbolic Computation | 2004-08-20 | Paper |
| scientific article; zbMATH DE number 2086593 (Why is no real title available?) | 2004-08-11 | Paper |
| scientific article; zbMATH DE number 2077140 (Why is no real title available?) | 2004-07-01 | Paper |
| scientific article; zbMATH DE number 2043528 (Why is no real title available?) | 2004-02-16 | Paper |
| scientific article; zbMATH DE number 1765694 (Why is no real title available?) | 2002-07-10 | Paper |
| A refinement-based approach to deriving train controllers | 2002-04-11 | Paper |
| scientific article; zbMATH DE number 1722701 (Why is no real title available?) | 2002-03-21 | Paper |
| scientific article; zbMATH DE number 1639660 (Why is no real title available?) | 2002-03-13 | Paper |
| On the construction of a domain language for a class of reactive systems | 2002-02-27 | Paper |
| scientific article; zbMATH DE number 1263399 (Why is no real title available?) | 2001-07-16 | Paper |
| scientific article; zbMATH DE number 1614706 (Why is no real title available?) | 2001-07-05 | Paper |
| scientific article; zbMATH DE number 1507181 (Why is no real title available?) | 2000-09-14 | Paper |
Using an induction prover for verifying arithmetic circuits
International Journal on Software Tools for Technology Transfer. STTT | 2000-01-01 | Paper |
| scientific article; zbMATH DE number 1253976 (Why is no real title available?) | 1999-07-14 | Paper |
| scientific article; zbMATH DE number 1254250 (Why is no real title available?) | 1999-07-06 | Paper |
| scientific article; zbMATH DE number 1256734 (Why is no real title available?) | 1999-06-21 | Paper |
Transformational methodology for proving termination of logic programs
The Journal of Logic Programming | 1998-11-05 | Paper |
| scientific article; zbMATH DE number 1189068 (Why is no real title available?) | 1998-08-13 | Paper |
Solving Polynomial Systems Using a Branch and Prune Approach
SIAM Journal on Numerical Analysis | 1997-11-02 | Paper |
New uses of linear arithmetic in automated theorem proving by induction
Journal of Automated Reasoning | 1996-11-04 | Paper |
A path ordering for proving termination of AC rewrite systems
Journal of Automated Reasoning | 1995-05-30 | Paper |
Complexity of unification problems with associative-commutative operators
Journal of Automated Reasoning | 1993-12-20 | Paper |
| scientific article; zbMATH DE number 408800 (Why is no real title available?) | 1993-09-06 | Paper |
| scientific article; zbMATH DE number 18651 (Why is no real title available?) | 1992-06-26 | Paper |
Sufficient-completeness, ground-reducibility and their complexity
Acta Informatica | 1991-01-01 | Paper |
Automating inductionless induction using test sets
Journal of Symbolic Computation | 1991-01-01 | Paper |
Semi-unification
Theoretical Computer Science | 1991-01-01 | Paper |
Inference rules and proof procedures for inequations
The Journal of Logic Programming | 1990-01-01 | Paper |
On ground-confluence of term rewriting systems
Information and Computation | 1990-01-01 | Paper |
Unnecessary inferences in associative-commutative completion procedures
Mathematical Systems Theory | 1990-01-01 | Paper |
| scientific article; zbMATH DE number 4132298 (Why is no real title available?) | 1989-01-01 | Paper |
Computing a Gröbner basis of a polynomial ideal over a Euclidean domain
Journal of Symbolic Computation | 1988-01-01 | Paper |
Only prime superpositions need be considered in the Knuth-Bendix completion procedure
Journal of Symbolic Computation | 1988-01-01 | Paper |
Wu's method and its application to perspective viewing
Artificial Intelligence | 1988-01-01 | Paper |
| scientific article; zbMATH DE number 4074541 (Why is no real title available?) | 1988-01-01 | Paper |
A refutational approach to geometry theorem proving
Artificial Intelligence | 1988-01-01 | Paper |
| scientific article; zbMATH DE number 4053061 (Why is no real title available?) | 1988-01-01 | Paper |
Computability and implementability issues in abstract data types
Science of Computer Programming | 1988-01-01 | Paper |
Problem corner: Proving equivalence of different axiomatizations of free groups
Journal of Automated Reasoning | 1988-01-01 | Paper |
A multi-level geometric reasoning system for vision
Artificial Intelligence | 1988-01-01 | Paper |
| scientific article; zbMATH DE number 4092757 (Why is no real title available?) | 1988-01-01 | Paper |
| scientific article; zbMATH DE number 4035205 (Why is no real title available?) | 1987-01-01 | Paper |
Complexity of matching problems
Journal of Symbolic Computation | 1987-01-01 | Paper |
On sufficient-completeness and related properties of term rewriting systems
Acta Informatica | 1987-01-01 | Paper |
Proof by consistency
Artificial Intelligence | 1987-01-01 | Paper |
Matching, unification and complexity
ACM SIGSAM Bulletin | 1987-01-01 | Paper |
Using Gröbner bases to reason about geometry problems
Journal of Symbolic Computation | 1986-01-01 | Paper |
| scientific article; zbMATH DE number 4049047 (Why is no real title available?) | 1986-01-01 | Paper |
| scientific article; zbMATH DE number 4047063 (Why is no real title available?) | 1986-01-01 | Paper |
| scientific article; zbMATH DE number 4011938 (Why is no real title available?) | 1986-01-01 | Paper |
| scientific article; zbMATH DE number 3930347 (Why is no real title available?) | 1985-01-01 | Paper |
| scientific article; zbMATH DE number 3921983 (Why is no real title available?) | 1985-01-01 | Paper |
A finite Thue system with decidable word problem and without equivalent finite canonical system
Theoretical Computer Science | 1985-01-01 | Paper |
The Knuth-Bendix Completion Procedure and Thue Systems
SIAM Journal on Computing | 1985-01-01 | Paper |
| scientific article; zbMATH DE number 3905845 (Why is no real title available?) | 1985-01-01 | Paper |
An \(O(| T| ^ 3)\) algorithm for testing the Church-Rosser property of Thue systems
Theoretical Computer Science | 1985-01-01 | Paper |
Worst-case choice for the stable marriage problem
Information Processing Letters | 1985-01-01 | Paper |
The Church-Rosser property and special Thue systems
Theoretical Computer Science | 1985-01-01 | Paper |
| scientific article; zbMATH DE number 3907753 (Why is no real title available?) | 1985-01-01 | Paper |
| scientific article; zbMATH DE number 3899033 (Why is no real title available?) | 1984-01-01 | Paper |
| scientific article; zbMATH DE number 3850464 (Why is no real title available?) | 1983-01-01 | Paper |
On Proving Uniform Termination and Restricted Termination of Rewriting Systems
SIAM Journal on Computing | 1983-01-01 | Paper |
| scientific article; zbMATH DE number 3759538 (Why is no real title available?) | 1982-01-01 | Paper |
| scientific article; zbMATH DE number 3911688 (Why is no real title available?) | 1982-01-01 | Paper |
