| Algorithms for computing greatest common divisors of parametric multivariate polynomials | 0 | 0.34 | 2021 |
| Conditional Congruence Closure over Uninterpreted and Interpreted Symbols. | 0 | 0.34 | 2019 |
| NIL: Learning Nonlinear Interpolants. | 1 | 0.35 | 2019 |
| Comprehensive Gröbner basis theory for a parametric polynomial ideal and the associated completion algorithm. | 0 | 0.34 | 2017 |
| Nonlinear Polynomials, Interpolants and Invariant Generation for System Analysis. | 0 | 0.34 | 2017 |
| Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF. | 1 | 0.35 | 2016 |
| Interpolation synthesis for quadratic polynomial inequalities and combination with \textit{EUF}. | 0 | 0.34 | 2016 |
| Unification and Matching in Hierarchical Combinations of Syntactic Theories | 0 | 0.34 | 2015 |
| When Is a Formula a Loop Invariant? | 0 | 0.34 | 2015 |
| On Asymmetric Unification and the Combination Problem in Disjoint Theories. | 0 | 0.34 | 2014 |
| An efficient method for computing comprehensive Gröbner bases | 6 | 0.48 | 2013 |
| Synthesizing switching controllers for hybrid systems by generating invariants | 6 | 0.40 | 2013 |
| On invariant checking. | 0 | 0.34 | 2013 |
| Elimination Techniques for Program Analysis. | 1 | 0.35 | 2013 |
| Harald Ganzinger's Legacy: Contributions to Logics and Programming. | 0 | 0.34 | 2013 |
| A "Hybrid" Approach for Synthesizing Optimal Controllers of Hybrid Systems: A Case Study of the Oil Pump Industrial Example | 6 | 0.41 | 2012 |
| Effective Symbolic Protocol Analysis via Equational Irreducibility Conditions. | 9 | 0.67 | 2012 |
| Program Analysis Using Quantifier-Elimination Heuristics - (Extended Abstract). | 0 | 0.34 | 2012 |
| Protocol analysis in Maude-NPA using unification modulo homomorphic encryption | 2 | 0.35 | 2011 |
| Termination Analysis of C Programs Using Compiler Intermediate Languages | 30 | 1.01 | 2011 |
| Coverset induction with partiality and subsorts: a powerlist case study | 3 | 0.38 | 2010 |
| Unification modulo a partial theory of exponentiation | 0 | 0.34 | 2010 |
| Idle port scanning and non-interference analysis of network protocol stacks using model checking | 18 | 1.27 | 2010 |
| A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs | 10 | 0.67 | 2009 |
| Identification of logically related heap regions | 7 | 0.47 | 2009 |
| Efficient context-sensitive shape analysis with graph based heap models | 14 | 0.87 | 2008 |
| Multivariate resultants in Bernstein basis | 0 | 0.34 | 2008 |
| Computer Mathematics: 8th Asian Symposium, ASCM 2007, Singapore, December 15-17, 2007. Revised and Invited Papers | 29 | 5.03 | 2008 |
| Identification of Heap---Carried Data Dependence Via Explicit Store Heap Models | 6 | 0.50 | 2008 |
| Heap analysis in the presence of collection libraries | 11 | 0.62 | 2007 |
| Dependency Pairs for Rewriting with Non-free Constructors | 4 | 0.42 | 2007 |
| Inductive decidability using implicit induction | 4 | 0.42 | 2006 |
| Third Special Issue on Techniques for Automated Termination Proofs | 1 | 0.36 | 2006 |
| A static heap analysis for shape and connectivity: unified memory analysis: the base framework | 7 | 0.52 | 2006 |
| Conditions for determinantal formula for resultant of a polynomial system | 2 | 0.37 | 2006 |
| Interpolation for data structures | 44 | 1.51 | 2006 |
| Bruno Buchberger — A life devoted to symbolic computation | 0 | 0.34 | 2006 |
| An Abstract Interpretation Approach for Automatic Generation of Polynomial Invariants | 29 | 1.62 | 2004 |
| Automatic generation of polynomial loop | 2 | 0.42 | 2004 |
| Program verification using automatic generation of invariants | 20 | 0.82 | 2004 |
| Support hull: relating the cayley-dixon resultant constructions to the support of a polynomial system | 0 | 0.34 | 2004 |
| Exact resultants for corner-cut unmixed multivariate polynomial systems using the Dixon formulation | 6 | 0.47 | 2003 |
| Model Checking Reconfigurable Processor Configurations for Safety Properties | 1 | 0.35 | 2003 |
| Automatic Generation of Simple Lemmas from Recursive Definitions Using Decision Procedures - Preliminary Report | 3 | 0.40 | 2003 |
| Deciding Inductive Validity of Equations | 7 | 0.49 | 2003 |
| On the relationship between the Dixon-based resultant construction and the supports of polynomial systems | 2 | 0.42 | 2003 |
| A Rewrite Rule Based Framework for Combining Decision Procedures | 7 | 0.60 | 2002 |
| Designing a Controller for a Multi-Train Multi-Track System | 1 | 0.43 | 2001 |
| Decidable Classes of Inductive Theorems | 12 | 0.66 | 2001 |
| Conditions for exact resultants using the Dixon formulation | 11 | 0.95 | 2000 |
