Reasoning on Procedural Programs using Description Logics with Concrete Domains
Ronald de Haan · 2012
Abstract. Existing approaches to assigning semantics to procedural programming languages do not easily allow automatic reasoning over programs. We assign a model theoretic semantics to programs of a simple procedural language, by encoding them into description logics with concrete domains. This allows us to flexibly express several reasoning problems over procedural programs, and to solve them efficiently using existing reasoning algorithms, for certain fragments of the programming language. Furthermore, it allows us to explore for what further fragments of the programming language reasoning problems are decidable. 1