Now showing items 53-72 of 100

    • 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 ...
    • Nonlocal Flow of Control and Kleene Algebra with Tests 

      Kozen, Dexter (2008-04-11)
      Kleene algebra with tests (KAT) is an equational system for program verification that combines Kleene algebra (KA), or the algebra of regular expressions, with Boolean algebra. It can model basic programming and verification ...
    • On Distance Coloring 

      Kozen, Dexter; Sharp, Alexa (Cornell University, 2007-06-29)
      Call a connected undirected graph (d,c)-colorable if there is a vertex coloring using at most c colors such that no two vertices of distance d or less have the same color. It is well known that (1,2)-colorability is ...
    • On Hoare Logic and Kleene Algebra with Tests 

      Kozen, Dexter (Cornell University, 1998-12)
      We show that Kleene algebra with tests subsumes propositional Hoare logic. Thus the specialized syntax and deductive apparatus of Hoare logic are inessential and can be replaced by ordinary equational reasoning. It follows ...
    • On Hoare Logic, Kleene Algebra, and Types 

      Kozen, Dexter (Cornell University, 1999-07)
      We show that propositional Hoare logic is subsumed by the type calculus of typed Kleene algebra augmented with subtypes and typecasting. Assertions are interpreted as typecast operators. Thus Hoare-style reasoning with ...
    • On Kleene Algebras and Closed Semirings 

      Kozen, Dexter (Cornell University, 1990-05)
      Kleene algebras are an important class of algebraic structures that arise in diverse areas of computer science: program logic and semantics, relational algebra, automata theory, and the design and analysis of algorithms. ...
    • On Moessner's Theorem 

      Kozen, Dexter; Silva, Alexandra (2011-06-12)
      Moessner's theorem describes a procedure for generating a sequence of n integer sequences that lead unexpectedly to the sequence of nth powers 1^n, 2^n, 3^n, ... Paasche's theorem is a generalization of Moessner's; by ...
    • On Parallelism in Turing Machines 

      Kozen, Dexter (Cornell University, 1976-06)
      A model of parallel computation based on a generalization of nondeterminism in Turing machines is introduced. Complexity classes //T(n)-TIME, //L(n)-SPACE, //LOGSPACE, //PTIME, etc. are defined for these machines in a ...
    • On Regularity-Preserving Functions 

      Kozen, Dexter (Cornell University, 1995-11)
      We give a characterization of regularity-preserving functions.
    • On Teaching Left-Handed Children to Write 

      Kozen, Dexter (Cornell University, 1987-06)
      It is argued that the handwriting method commonly taught to left-handed children is incorrect and harmful. The disadvantages of this method are noted, and a new method alleviating these disadvantages is proposed.
    • On the Coalgebraic Theory of Kleene Algebra with Tests 

      Kozen, Dexter (2008-03-14)
      We develop a coalgebraic theory of Kleene algebra with tests (KAT) along the lines of Rutten (1998) for Kleene algebra (KA) and Chen and Pucella (2003) for a limited version of KAT, resolving two open problems of Chen and ...
    • On the Completeness of Propositional Hoare Logic 

      Kozen, Dexter; Tiuryn, Jerzy (Cornell University, 1999-09)
      We investigate the completeness of Hoare Logic on the propositional level. In particular, the expressiveness requirements of Cook's proof are characterized propositionally. We give a completeness result for Propositional ...
    • On the Complexity of Reasoning in Kleene Algebra 

      Kozen, Dexter (Cornell University, 1997-03)
      We study the complexity of reasoning in Kleene algebra and *-continuous Kleene algebra in the presence of extra equational assumptions $E$; that is, the complexity of deciding the validity of universal Horn formulas $E\imp ...