Skip to main content


eCommons@Cornell

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

Files in This Item:

File SizeFormat
TR2003-1915.ps409.87 kBPostscriptView/Open

Refworks Export

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.

 

© 2014 Cornell University Library Contact Us