Static analysis of programs using Omega algebra with tests

Abstract

Recently, Kozen has proposed a framework based on Kleene algebra with tests for verifying that a program satisfies a security policy specified by a security automaton. A security automaton is used for the specification of linear safety properties on finite and infinite runs. This kind of property is very interesting for most common programs. However, it is not possible to specify liveness properties with security automata. In this paper, we use omega algebra with tests and automata on infinite words to extend the field of properties that can be handled by security automata in Kozen's framework. © Springer-Verlag Berlin Heidelberg 2006.