Kleene Algebra with Tests and the Static Analysis of Programs

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Nov 17, 2003
Accession Number
AD1001031

Entities

People

  • Dexter Kozen

Organizations

  • Cornell University

Tags

Communities of Interest

  • Energy and Power Technologies

DTIC Thesaurus Topics

  • Alphabets
  • Artificial Intelligence
  • Automata
  • Basic Programming Language
  • Boolean Algebra
  • Computations
  • Computer Programming
  • Computer Science
  • Computers
  • Device Drivers
  • Equations
  • Finite Alphabet
  • Formal Languages
  • Language
  • Logic
  • Models
  • Programming Languages
  • Relational Database Management Systems
  • Security
  • Sequences
  • Theorems
  • Transitions
  • Verification

Fields of Study

  • Computer science
  • Mathematics

Readers

  • Database Systems and Applications
  • Mathematical Modeling and Probability Theory.