Kleene Algebra with Tests and the Static Analysis of Programs
MetadataShow full item record
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.
computer science; technical report
Previously Published As