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

Malicious Code Detection for Open Firmware
Adelstein, Frank; Stillerman, Matt; Kozen, Dexter (Cornell University, 20020927)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 (20140521)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 ... 
MyhillNerode Relations on Automatic Systems and the Completeness ofKleene Algebra
Kozen, Dexter (Cornell University, 20001130)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, 20040702)Eklund et al. (2002) present a graphical technique aimed at simplifying the verification of various categorytheoretic 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, 198612)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, JeanBaptiste; Kozen, Dexter; Schlesinger, Cole; Walker, David (20131011)Recent years have seen growing interest in highlevel 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 (20120317)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 objectoriented languages ... 
Nominal Kleene Coalgebra
Kozen, Dexter; Mamouras, Konstantinos; Petrisan, Daniela; Silva, Alexandra (20150218)We develop the coalgebraic theory of nominal Kleene algebra, including an alternative languagetheoretic semantics, a nominal extension of the Brzozowski derivative, and a bisimulationbased decision procedure for the ... 
Nonlocal Flow of Control and Kleene Algebra with Tests
Kozen, Dexter (20080411)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, 20070629)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, 199812)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, 199907)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 Hoarestyle reasoning with ... 
On Kleene Algebras and Closed Semirings
Kozen, Dexter (Cornell University, 199005)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 (20110612)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, 197606)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 RegularityPreserving Functions
Kozen, Dexter (Cornell University, 199511)We give a characterization of regularitypreserving functions. 
On Teaching LeftHanded Children to Write
Kozen, Dexter (Cornell University, 198706)It is argued that the handwriting method commonly taught to lefthanded 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 (20080314)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, 199909)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, 199703)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 ...