Now showing items 25-44 of 100

    • 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 ...
    • First Order Predicate Logic Without Negation is NP-Complete 

      Kozen, Dexter (Cornell University, 1977-04)
      Techniques developed in the study of the complexity of finitely presented algebras are used to show that the problem of deciding validity of positive sentences in the language of first order predicate logic with equality ...
    • Functional Decomposition of Polynomials 

      Von zur Gathen, Joachim; Kozen, Dexter; Landau, Susan (Cornell University, 1987-07)
    • Halting and Equivalence of Program Schemes in Models of Arbitrary Theories 

      Kozen, Dexter (2010-05-19)
      In this note we consider the following decision problems. Let S be a fixed first-order signature. (i) Given a first-order theory or ground theory T over S of Turing degree A, a program scheme p over S, and input values ...
    • Halting and Equivalence of Schemes over Recursive Theories 

      Kozen, Dexter (Cornell University, 2002-10-28)
      Let S be a fixed first-order signature. In this note we consider the following decision problems. (i) Given a recursive ground theory T over S, a program scheme p over S, and input values specified by ground terms ...
    • Indefinite Summation and the Kronecker Delta 

      Kozen, Dexter; Timme, Marc (2007-10-18)
      Indefinite summation, together with a generalized version of the Kronecker delta, provide a calculus for reasoning about various polynomial functions that arise in combinatorics, such as the Tutte, chromatic, flow, and ...
    • Infinitary Axiomatization of the Equational Theory of Context-Free Languages 

      Grathwohl, Niels Bjørn Bugge; Henglein, Fritz; Kozen, Dexter (2013-07-01)
      We give a natural complete infinitary axiomatization of the equational theory of the context-free languages, answering a question of Leiss (1992).
    • Intuitionistic Linear Logic and Partial Correctness 

      Kozen, Dexter; Tiuryn, Jerzy (Cornell University, 2001-01-02)
      We formulate a Gentzen-style sequent calculus for partial correctness that subsumes propositional Hoare Logic. The system is a noncommutative Intuitionistic Linear Logic. We prove soundness and completeness over relational ...
    • KAT + B! 

      Grathwohl, Niels Bjørn Bugge; Kozen, Dexter; Mamouras, Konstantinos (2014-01-08)
      It is known that certain program transformations require a small amount of mutable state, a feature not explicitly provided by Kleene algebra with tests (KAT). In this paper we show how to axiomatically extend KAT with ...
    • KAT-ML: An Interactive Theorem Prover for Kleene Algebra with Tests 

      Aboul-Hosn, Kamal; Kozen, Dexter (Cornell University, 2003-08-21)
      KAT-ML is an interactive theorem prover for Kleene algebra with tests (KAT). The system is designed to reflect the natural style of reasoning with KAT that one finds in the literature. We describe the main features of ...
    • Kleene Algebra and Bytecode Verification 

      Kot, Lucja; Kozen, Dexter (Cornell University, 2004-12-20)
      Most standard approaches to the static analysis of programs, such as the popular worklist method, are first-order methods that inductively annotate program points with abstract values. In a recent paper we introduced a ...
    • Kleene Algebra with Equations 

      Kozen, Dexter; Mamouras, Konstantinos (2014-02-27)
      We identify sufficient conditions for the construction of free language models for systems of Kleene algebra with additional equations. The construction applies to a broad class of extensions of KA and provides a uniform ...
    • Kleene algebra with tests and commutativity conditions 

      Kozen, Dexter (Cornell University, 1996-01)
      We give an equational proof, using Kleene algebra with tests and commutativity conditions, of the following classical result: every while program can be simulated by a while program with at most one while loop. The proof ...
    • Kleene Algebra with Tests and Program Schematology 

      Angus, Allegra; Kozen, Dexter (Cornell University, 2001-07-10)
      The theory of flowchart schemes has a rich history going back to Ianov (1960); see Manna (1974) for an elementary exposition. A central question in the theory of program schemes is scheme equivalence. Manna presents ...