|
eCommons@Cornell >
Faculty of Computing and Information Science >
Computing and Information Science >
Computing and Information Science Technical Reports >
Please use this identifier to cite or link to this item:
http://hdl.handle.net/1813/5627
| Title: | Kleene Algebra with Tests and the Static Analysis of Programs |
| Authors: | Kozen, Dexter |
| Keywords: | computer science
technical report |
| Issue Date: | 17-Nov-2003 |
| Publisher: | Cornell University |
| Citation: | http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cis/TR2003-1915 |
| Abstract: | 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. We prove soundness and completeness over relational interpretations. We illustrate the method on an example involving the correctness of a device driver. |
| URI: | http://hdl.handle.net/1813/5627 |
| Appears in Collections: | Computing and Information Science Technical Reports
|
Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.
|
