Now showing items 34-53 of 100

    • 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 ...
    • 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 ...