-
Chapter and Conference Paper
D-bases for polynomial ideals over commutative noetherian rings
We present a completion-like procedure for constructing D-bases for polynomial ideals over commutative Noetherian rings with. unit. The procedure is described at an abstract level, by transition rules. Its termin...
-
Chapter and Conference Paper
Rigid E-Unification Revisited
This paper presents a sound and complete set of abstract transformation rules for rigid E-unification. Abstract congruence closure, syntactic unification and paramodulation are the three main components of the pr...
-
Chapter and Conference Paper
Abstract Congruence Closure and Specializations
We use the uniform framework of abstract congruence closure to study the congruence closure algorithms described by Nelson and Oppen [9], Downey, Sethi and Tarjan [7], and Shostak [11]. The descriptions thus obta...
-
Chapter and Conference Paper
Rewrite Closure for Ground and Cancellative AC Theories
Given a binary relation on the set of ground terms over some signature, we define an abstract rewrite closure for
-
Chapter and Conference Paper
Series of Abstractions for Hybrid Automata
We present a technique based on the use of the quantifier elimination decision procedure for real closed fields and simple theorem proving to construct a series of successively finer qualitative abstractions o...
-
Chapter and Conference Paper
Approximate Reachability for Linear Systems
We describe new techniques to construct, and subsequently refine, over-approximations of the reachability sets for linear dynamical systems. Our approach extracts information from real eigenvectors and more ge...
-
Chapter and Conference Paper
On the Confluence of Linear Shallow Term Rewrite Systems
We show that the confluence of shallow linear term rewrite systems is decidable. The decision procedure is a nontrivial generalization of the polynomial time algorithms for deciding confluence of ground and re...
-
Chapter and Conference Paper
Automated Symbolic Reachability Analysis; with Application to Delta-Notch Signaling Automata
This paper describes the implementation of predicate abstraction techniques to automatically compute symbolic backward reachable sets of high dimensional piecewise affine hybrid automata, used to model Delta-N...
-
Article
Abstract Congruence Closure
We describe the concept of an abstract congruence closure and provide equational inference rules for its construction. The length of any maximal derivation using these inference rules for constructing an abstract...
-
Chapter and Conference Paper
SAL 2
SAL (see http://sal.csl.sri.com) is an open suite of tools for analysis of state machines; it constitutes part of our vision for a Symbolic Analysis Laboratory that will eventually encompass SAL, the PVS verifica...
-
Chapter and Conference Paper
Termination of Linear Programs
We show that termination of a class of linear loop programs is decidable. Linear loop programs are discrete-time linear systems with a loop condition governing termination, that is, a while loop with linear as...
-
Chapter and Conference Paper
Deciding Fundamental Properties of Right-(Ground or Variable) Rewrite Systems by Rewrite Closure
Right-(ground or variable) rewrite systems (RGV systems for short) are term rewrite systems where all right hand sides of rules are restricted to be either ground or a variable. We define a minimal rewrite ext...
-
Chapter and Conference Paper
Nonlinear Systems: Approximating Reach Sets
We describe techniques to generate useful reachability information for nonlinear dynamical systems. These techniques can be automated for polynomial systems using algorithms from computational algebraic geomet...
-
Chapter and Conference Paper
Symbolic Systems Biology: Hybrid Modeling and Analysis of Biological Networks
How do living cells compute and control themselves, and communicate with their environment? We describe the modeling and analysis of dynamic and reactive biological systems involving both discrete and continuo...
-
Article
Characterizing Confluence by Rewrite Closure and Right Ground Term Rewrite Systems
Just as saturation under an appropriate superposition calculus leads to a convergent presentation of a given equational theory, saturation under a suitable chaining calculus gives, what we call, a rewrite clos...
-
Chapter and Conference Paper
Termination of Rewrite Systems with Shallow Right-Linear, Collapsing, and Right-Ground Rules
We show that termination is decidable for rewrite systems that contain shallow and right-linear rules, collapsing rules, and right-ground rules. This class of rewrite systems is expressive enough to include in...
-
Chapter and Conference Paper
Generating Polynomial Invariants for Hybrid Systems
We present a powerful computational method for automatically generating polynomial invariants of hybrid systems with linear continuous dynamics. When restricted to linear continuous dynamical systems, our meth...
-
Chapter and Conference Paper
Confluence of Shallow Right-Linear Rewrite Systems
We show that confluence of shallow and right-linear term rewriting systems is decidable. This class of rewriting system is expressive enough to include nontrivial nonground rules such as commutativity, identit...
-
Chapter and Conference Paper
An Algebraic Approach for the Unsatisfiability of Nonlinear Constraints
We describe a simple algebraic semi-decision procedure for detecting unsatisfiability of a (quantifier-free) conjunction of nonlinear equalities and inequalities. The procedure consists of Gröbner basis comput...
-
Chapter and Conference Paper
Join Algorithms for the Theory of Uninterpreted Functions
The join of two sets of facts, E 1 and E 2, is defined as the set of all facts that are implied independently by both E 1 and E ...
