JavaScript is disabled for your browser. Some features of this site may not work without it.
Browsing by Author "Kozen, Dexter"
Now showing items 1231 of 100

A Complete Gentzenstyle Axiomatization for Set Constraints
Cheng, Allan; Kozen, Dexter (Cornell University, 199505)Set constraints are inclusion relations between expressions denoting sets of ground terms over a ranked alphabet. They are the main ingredient in setbased program analysis. In this paper we provide a Gentzenstyle ... 
Completeness and Incompleteness in Nominal Kleene Algebra
Kozen, Dexter; Mamouras, Konstantinos; Silva, Alexandra (20141114)Gabbay and Ciancia (2011) presented a nominal extension of Kleene algebra as a framework for trace semantics with dynamic allocation of resources, along with a semantics consisting of nominal languages. They also provided ... 
A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events
Kozen, Dexter (Cornell University, 199005)We give a finite axiomatization of the algebra of regular events involving only universal Horn formulas. Unlike Salomaa's axiomatizations, ours is sound for all interpretations over Kleene algebras. 
Complexity of Finitely Presented Algebras
Kozen, Dexter (Cornell University, 197612)An algebra $\cal A$ is finitely presented if there is a finite set G of generator symbols, a finite set O of operator symbols, and a finite set $\Gamma$ of defining relations $x \equiv y$ where $x$ and $y$ are wellformed ... 
The Complexity of Kleene Algebra with Tests
Cohen, Ernie; Kozen, Dexter; Smith, Frederick (Cornell University, 199607)Kleene algebras with tests provide a natural framework for equational specification and verification. Kleene algebras with tests and related systems have been used successfully in basic safety analysis, sourcetosource ... 
The Complexity of Set Constraints
Aiken, Alexander; Kozen, Dexter; Vardi, Moshe; Wimmers, Ed (Cornell University, 199305)Set constraints are relations between sets of terms. They have been used extensively in various applications in program analysis and type inference. We present several results on the computational complexity of solving ... 
Computational Inductive Definability
Kozen, Dexter (Cornell University, 20020403)It is shown that over any countable firstorder structure, IND programs with dictionaries accept exactly the Pi11 relations. This extends a result of Harel and Kozen (1984) relating IND and Pi11 over countable structures ... 
Computing the Newtonian Graph (Extended abstract)
Kozen, Dexter; Stefansson, Kjartan (Cornell University, 199310)A polynomial $f\in \complex[z]$ defines a vector field $N_f(z) = f(z)/f'(z)$ on $\complex$. Certain degenerate curves of flow in $N_f$ give the edges of the Newtonian graph, as defined by \cite{Sma85}. These give ... 
Computing with Capsules
Jeannin, JeanBaptiste; Kozen, Dexter (20110126)Capsules provide a clean algebraic representation of the state of a computation in higherorder functional and imperative languages. They play the same role as closures or heap or stackallocated environments but are ... 
A Conversation with Dexter Kozen
Kozen, Dexter; Constable, Robert L. (InternetFirst University Press, 20150909)Kozen discusses his experiences at Cornell – his research and teaching experience, textbooks, participation in sports & music, etc. 
Decidability of Systems of Set Constraints with Negative Constraints
Aiken, Alexander; Kozen, Dexter; Wimmers, Ed (Cornell University, 199306)Set constraints are relations between sets of terms. They have been used extensively in various applications in program analysis and type inference. Recently, several algorithms for solving general systems of positive ... 
Decomposition of Algebraic Functions
Kozen, Dexter; Landau, Susan; Zippel, Richard (Cornell University, 199402)Functional decompositionwhether a function $f(x)$ can be written as a composition of functions $g(h(x))$ in a nontrivial wayis an important primitive in symbolic computation systems. The problem of univariate ... 
Definability with Bounded Number of Bound Variables
Immerman, Neil; Kozen, Dexter (Cornell University, 198703)A theory satisfies the $k$variableproperty if every firstorder formula is equivalent to a formula with at most $k$ bound variables (possibly reused). Gabbay has shown that a fixed time structure satisfies the $k$variable ... 
Eager Class Initialization for Java
Kozen, Dexter; Stillerman, Matt (Cornell University, 20010723)We describe a static analysis method on Java bytecode to determine class initialization dependencies. This method can be used for eager class loading and initialization. It catches many initialization circularities that ... 
Efficient Algorithms for Optimal Video Transmission
Kozen, Dexter; Minsky, Yaron; Smith, Brian (Cornell University, 199505)This paper addresses the problem of sending an encoded video stream over a channel of limited bandwidth. When there is insufficient bandwidth available, some data must be dropped. For many video encodings, some data are ... 
Efficient AverageCase Algorithms for the Modular Group
Kozen, Dexter (Cornell University, 199404)The modular group occupies a central position in many branches of mathematical sciences. In this paper we give average polynomialtime algorithms for the unbounded and bounded membership problems for finitely generated ... 
Efficient Code Certification
Kozen, Dexter (Cornell University, 199801)We introduce a simple and efficient approach to the certification of compiled code. We ensure a basic but nontrivial level of code safety, including control flow safety, memory safety, and stack safety. The system is ... 
Efficient Resolution of Singularities of Plane Curves
Kozen, Dexter (Cornell University, 199404)We give a new algorithm for resolving singularities of plane curves. The algorithm is polynomial time in the bit complexity model, does not require factorization, and works over the rationals or finite fields. 
Equational Verification of Cache Blocking in LU Decomposition using Kleene Algebra with Tests
Barth, Adam; Kozen, Dexter (Cornell University, 20021024)In a recent paper of Mateev et al. (2001), a new technique for program analysis called fractal symbolic analysis was introduced and applied to verify the correctness of a series of sourcelevel transformations for cache ... 
Finitely Presented Algebras and the Polynomial Time Hiercharchy
Kozen, Dexter (Cornell University, 197703)Let $S_{n}(V_{n})=\{less than \Gamma, Q_{1}v_{1}\cdots Q_{k}v_{k} s \equiv j greater than  \Gamma$ is a finite presentation of $\cal A, Q_{1} \cdots Q_{k}$ is a string of quantifiers with $n$ alterations, the outermost ...