Imperative programming languages are ubiquitous in virtually all fields of technology, with programs specifying all sorts of computational behavior. For many practical reasons, an automated analysis of semantic properties of programs, such as termination and equivalence, is desirable. We provide a new approach to the automated semantic analysis of programs by encoding their behavior into formal logic. We consider a few syntactically simple imperative programming languages, and we encode programs of these languages into expressions of the description logic ALC(D) for a particular domain D. We do this in such a way that models of these encodings correspond to executions of the source programs. In other words, essentially, we assign a model-theoretic semantics to imperative programs. This encoding makes it possible to express semantic properties of programs (most notably termination and equivalence) in the formal logic language. Effectively, in this fashion, we reduce reasoning problems defined on the programs to description logic reasoning.
Practically, this directly results in algorithms to perform automated reasoning on a number of restricted fragments of the programming languages (i.e. loop-free programs, or programs restricted to a finite numerical domain). Theoretically, our approach makes it possible to identify further, less restricted fragments of the programming languages for which certain reasoning tasks are decidable. We identify one such fragment, based on finite partitionings of the state space, and illustrate what class of programs belongs to this fragment.