Now showing items 41-60 of 100

    • 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 ...
    • Kleene Algebra with Tests and the Static Analysis of Programs 

      Kozen, Dexter (Cornell University, 2003-11-17)
      We propose a general framework for the static analysis of programs based on Kleene algebra with tests (KAT). We show how KAT can be used to statically verify compliance with safety policies specified by security automata. ...
    • Kleene Algebra with Tests: Completeness and Decidability 

      Kozen, Dexter; Smith, Frederick (Cornell University, 1996-04)
      Kleene algebras with tests provide a rigorous framework for equational specification and verification. They have been used successfully in basic safety analysis, source-to-source program transformation, and concurrency ...
    • Kolmogorov Extension, Martingale Convergence, and Compositionality of Processes 

      Kozen, Dexter (2015-12-30)
      We show that the Kolmogorov extension theorem and the Doob martingale convergence theorem are two aspects of a common generalization, namely a colimit-like construction in a category of Radon spaces and reversible Markov ...
    • Language-Based Security 

      Kozen, Dexter (Cornell University, 1999-06)
      Security of mobile code is a major issue in today's global computing environment. When you download a program from an untrusted source, how can you be sure it will not do something undesirable? In this paper I will discuss ...
    • Left-Handed Completeness 

      Kozen, Dexter; Silva, Alexandra (2011-08-23)
      We give a new, significantly shorter proof of the completeness of the left-handed star rule of Kleene algebra. The proof reveals the rich interaction of algebra and coalgebra in the theory.
    • Lexicographic Flow 

      Kozen, Dexter (2009-06-25)
      The lexicographic flow problem is a flow problem in which the edges are assigned priorities, and we wish to find a flow that is lexicographically maximum with respect to the priority assignment. The problem is reducible ...
    • Logical Aspects of Set Constraints 

      Kozen, Dexter (Cornell University, 1994-05)
      Set constraints are inclusion relations between sets of ground terms over a ranked alphabet. They have been used extensively in program analysis and type inference. Here we present an equational axiomatization of the ...
    • Logics of Programs 

      Kozen, Dexter; Tiuryn, Jerzy (Cornell University, 1989-01)
      None Available
    • Malicious Code Detection for Open Firmware 

      Adelstein, Frank; Stillerman, Matt; Kozen, Dexter (Cornell University, 2002-09-27)
      Malicious boot firmware is a largely unrecognized but significant security risk to our global information infrastructure. Since boot firmware executes before the operating system is loaded, it can easily circumvent any ...
    • A Metrized Duality Theorem for Markov Processes 

      Kozen, Dexter; Mardare, Radu; Panangaden, Prakash (2014-05-21)
      We extend our previous duality theorem for Markov processes by equipping the processes with a pseudometric and the algebras with a notion of metric diameter. We are able to show that the isomorphisms of our previous duality ...
    • Myhill-Nerode Relations on Automatic Systems and the Completeness ofKleene Algebra 

      Kozen, Dexter (Cornell University, 2000-11-30)
      It is well known that finite square matrices over a Kleene algebra again form a Kleene algebra. This is also true for infinite matrices under suitable restrictions. One can use this fact to solve certain infinite systems ...
    • Natural Transformations as Rewrite Rules and Monad Composition 

      Kozen, Dexter (Cornell University, 2004-07-02)
      Eklund et al. (2002) present a graphical technique aimed at simplifying the verification of various category-theoretic constructions, notably the composition of monads. In this note we take a different approach involving ...
    • NC Algorithms for Comparability Graphs, Interval Graphs, and Unique Perfect Matchings 

      Kozen, Dexter; Vazirani, Umesh V.; Vazirani, Vijay V. (Cornell University, 1986-12)
      Laszlo Lovasz recently posed the following problem: "Is there an NC algorithm for testing if a given graph has a unique perfect matching?" We present such an algorithm for bipartite graphs. We also give NC algorithms ...
    • NetKAT: Semantic Foundations for Networks 

      Anderson, Carolyn Jane; Foster, Nate; Guha, Arjun; Jeannin, Jean-Baptiste; Kozen, Dexter; Schlesinger, Cole; Walker, David (2013-10-11)
      Recent years have seen growing interest in high-level languages for programming networks. But the design of these languages has been largely ad hoc, driven more by the needs of applications and the capabilities of network ...
    • New 

      Kozen, Dexter (2012-03-17)
      We propose a theoretical device for modeling the creation of new indiscernible semantic objects during program execution. The method fits well with the semantics of imperative, functional, and object-oriented languages ...
    • Nominal Kleene Coalgebra 

      Kozen, Dexter; Mamouras, Konstantinos; Petrisan, Daniela; Silva, Alexandra (2015-02-18)
      We develop the coalgebraic theory of nominal Kleene algebra, including an alternative language-theoretic semantics, a nominal extension of the Brzozowski derivative, and a bisimulation-based decision procedure for the ...