KIT | KIT-Bibliothek | Impressum
Open Access Logo
URN: urn:nbn:de:swb:90-AAA267961

Verification of a Prolog compiler - first steps with KIV

Schellhorn, Gerhard; Ahrendt, Wolfgang


This paper describes the first steps of the formal verification of
a Prolog compiler with the KIV system. We build upon the mathematical
definitions given by Boerger and Rosenzweig in [BR95]. There an
operational semantics of Prolog is defined using the formalism of
Evolving Algebras, and then transformed in several systematic steps
to the Warren Abstract Machine (WAM). To verify these transformation
steps formally in KIV, a translation of deterministic Evolving
Algebras to Dynamic Logic is defined, which may also be of general
interest. With this translation, correctness of transformation steps
becomes a problem of program equivalence in Dynamic Logic. We define
a proof technique for verifying such problems, which corresponds to
the use of proof maps in Evolving Algebras. Although the transfor-
mation steps are small enough for a mathematical analysis, this is not
sufficient for a successful formal correctness proof. Such a proof
requires to explicitly state a lot of facts, which were only impli-
citly assumed in the analysis.
We will argue that these assumptions cannot be guessed in a first
proof attempt, but have to be filled in ... mehr

Zugehörige Institution(en) am KIT Institut für Logik, Komplexität und Deduktionssysteme (ILKD)
Publikationstyp Buch
Jahr 1996
Sprache Englisch
Identifikator KITopen ID: 26796
Erscheinungsvermerk Karlsruhe 1996. (Interner Bericht. Fakultät für Informatik, Universität Karlsruhe. 1996,27.)
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page