Dexter Kozen. On Hoare Logic, Kleene Algebra, and Types. In P. Gärdenfors, J. Wolenski, and K. Kijania-Placek, editors, In the Scope of Logic, Methodology, and Philosophy of Science: Volume 1 of the 11th Int. Congress Logic, Methodology and Philosophy of Science, Cracow, August 1999, volume 315 of Studies in Epistemology, Logic, Methodology, and Philosophy of Science, pages 119-133. Kluwer, 2002.
[full text (.pdf)]
[bibtex]
[top]
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 partial correctness assertions reduces to typechecking in this system.
[top]
Robert Givan, David McAllester, Carl Witty and Dexter Kozen. Tarskian Set Constraints. Information and Computation, 174(2):105-131, May 2002.
[full text (.ps)]
[bibtex]
[top]
We investigate set constraints over set expressions with Tarskian functional and relational operations. Unlike the Herbrand constructor symbols used in recent set constraint formalisms, the meaning of a Tarskian function symbol is interpreted in an arbitrary first order structure. We show that satisfiability of Tarskian set constraints is decidable in nondeterministic doubly exponential time. We also give complexity results and open problems for various extensions and restrictions of the language.
[top]
Dexter Kozen. On the Complexity of Reasoning in Kleene Algebra. Information and Computation 179, 152-162, 2002.
[full text (.pdf)]
[bibtex]
[top]
We study the complexity of reasoning in Kleene algebra and *-continuous Kleene algebra in the presence of extra assumptions; i.e., the complexity of deciding the validity of universal Horn formulas E --> s=t, where E is a finite set of equations. We obtain various levels of complexity based on the form of the assumptions E. Our main results are: for *-continuous Kleene algebra,
1. if E contains only commutativity assumptions pq=qp, the problem is Pi-0-1-complete (co-r.e. complete);
2. if E contains only monoid equations, the problem is Pi-0-2-complete;
3. for arbitrary equations E, the problem is Pi-1-1-complete.
The last problem is the universal Horn theory of the *-continuous Kleene algebras. This resolves an open question of [Kozen, LICS 1991].
[top]
Dexter Kozen. Halting and Equivalence of Schemes over Recursive Theories. Technical Report TR2002-1881, Computer Science Department, Cornell University, October 2002.
[full text (.pdf)]
[bibtex]
[top]
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 t1,...,tn, does p halt on input t1,...,tn in all models of T? (ii) Given a recursive ground theory T over S and two program schemes p and q over S, are p and q equivalent in all models of T? When T is empty, these two problems are the classical halting and equivalence problems for program schemes, respectively. We show that problem (i) is r.e.-complete and problem (ii) is Pi-0-2-complete. Both these problems remain hard for their respective complexity classes even if T is empty and S is restricted to contain only a single constant, a single unary function symbol, and a single monadic predicate. It follows from (ii) that there can exist no relatively complete deductive system for scheme equivalence.
[top]
Chris Hardin and Dexter Kozen. On the Elimination of Hypotheses in Kleene Algebra with Tests. Technical Report TR2002-1879, Computer Science Department, Cornell University, October 2002.
[full text (.pdf)]
[bibtex]
[top]
The validity problem for certain universal Horn formulas of Kleene algebra with tests (KAT) can be efficiently reduced to the equational theory. This reduction is known as elimination of hypotheses. Hypotheses are used to describe the interaction of atomic programs and tests and are an essential component of practical program verification with KAT. The ability to eliminate hypotheses of a certain form means that the Horn theory with premises of that form remains decidable in PSPACE. It was known (Cohen 1994, Kozen and Smith 1996, Kozen 1997) how to eliminate hypotheses of the form q=0. In this paper we show how to eliminate hypotheses of the form cp=c for atomic p. Hypotheses of this form are useful in eliminating redundant code and arise quite often in the verification of compiler optimizations (Kozen and Patron 2000).
[top]
Frank Adelstein, Dexter Kozen and Matt Stillerman. Malicious Code Detection for Open Firmware. In Proc. 18th Computer Security Applications Conf. (ACSAC'02), Las Vegas, December 2002, pages 403-412.
[full text (.pdf)]
[bibtex]
[top]
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 operating system-based security mechanism. Boot firmware programs are typically written by third-party device manufacturers and may come from various suppliers of unknown origin. In this paper we describe an approach to this problem based on load-time verification of onboard device drivers against a standard security policy designed to limit access to system resources. We also describe our ongoing effort to construct a prototype of this technique for Open Firmware boot platforms.
[top]
Adam Barth and Dexter Kozen. Equational Verification of Cache Blocking in LU Decomposition using Kleene Algebra with Tests. Technical Report TR2002-1865, Computer Science Department, Cornell University, June 2002.
[full text (.pdf)]
[bibtex]
[top]
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 blocking in LU decomposition with partial pivoting. It was argued in that paper that traditional techniques are inadequate because the transformations break definition-use dependencies. We show how the task can be accomplished purely equationally using Kleene algebra with tests.
[top]
Dexter Kozen. On Two Letters versus Three. Technical Report 2002-1860, Computer Science Department, Cornell University, February 2002.
[full text (.pdf)]
[bibtex]
[top]
If A is a context-free language over a two-letter alphabet, then the set of all words obtained by sorting words in A and the set of all permutations of words in A are context-free. This is false over alphabets of three or more letters. Thus these problems illustrate a difference in behavior between two- and three-letter alphabets.
[top]
Dexter Kozen and Matt Stillerman. Eager Class Initialization for Java. In W. Damm and E.R. Olderog, editors, Proc. 7th Int. Symp. Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT'02), volume 2469 of Lecture Notes in Computer Science, pages 71-80. IFIP, Springer-Verlag, Sept. 2002.
[full text (.pdf)]
[bibtex]
[top]
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 are missed by the standard lazy implementation. Except for contrived examples, the computed initialization order gives the same results as standard lazy initialization.
[top]