Now showing items 12-31 of 100

    • A Complete Gentzen-style Axiomatization for Set Constraints 

      Cheng, Allan; Kozen, Dexter (Cornell University, 1995-05)
      Set constraints are inclusion relations between expressions denoting sets of ground terms over a ranked alphabet. They are the main ingredient in set-based program analysis. In this paper we provide a Gentzen-style ...
    • Completeness and Incompleteness in Nominal Kleene Algebra 

      Kozen, Dexter; Mamouras, Konstantinos; Silva, Alexandra (2014-11-14)
      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, 1990-05)
      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, 1976-12)
      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 well-formed ...
    • The Complexity of Kleene Algebra with Tests 

      Cohen, Ernie; Kozen, Dexter; Smith, Frederick (Cornell University, 1996-07)
      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, source-to-source ...
    • The Complexity of Set Constraints 

      Aiken, Alexander; Kozen, Dexter; Vardi, Moshe; Wimmers, Ed (Cornell University, 1993-05)
      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, 2002-04-03)
      It is shown that over any countable first-order structure, IND programs with dictionaries accept exactly the Pi-1-1 relations. This extends a result of Harel and Kozen (1984) relating IND and Pi-1-1 over countable structures ...
    • Computing the Newtonian Graph (Extended abstract) 

      Kozen, Dexter; Stefansson, Kjartan (Cornell University, 1993-10)
      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, Jean-Baptiste; Kozen, Dexter (2011-01-26)
      Capsules provide a clean algebraic representation of the state of a computation in higher-order functional and imperative languages. They play the same role as closures or heap- or stack-allocated environments but are ...
    • A Conversation with Dexter Kozen 

      Kozen, Dexter; Constable, Robert L. (Internet-First University Press, 2015-09-09)
      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, 1993-06)
      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, 1994-02)
      Functional decomposition--whether a function $f(x)$ can be written as a composition of functions $g(h(x))$ in a nontrivial way--is an important primitive in symbolic computation systems. The problem of univariate ...
    • Definability with Bounded Number of Bound Variables 

      Immerman, Neil; Kozen, Dexter (Cornell University, 1987-03)
      A theory satisfies the $k$-variable-property if every first-order 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, 2001-07-23)
      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, 1995-05)
      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 Average-Case Algorithms for the Modular Group 

      Kozen, Dexter (Cornell University, 1994-04)
      The modular group occupies a central position in many branches of mathematical sciences. In this paper we give average polynomial-time algorithms for the unbounded and bounded membership problems for finitely generated ...
    • Efficient Code Certification 

      Kozen, Dexter (Cornell University, 1998-01)
      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, 1994-04)
      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, 2002-10-24)
      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 source-level transformations for cache ...
    • Finitely Presented Algebras and the Polynomial Time Hiercharchy 

      Kozen, Dexter (Cornell University, 1977-03)
      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 ...