Specify in RSL and Prove in Isabelle

Morten Peter Lindegaard

    Research output: Contribution to conference › Poster › Research

    Abstract

    An approach to increasing proof support for the RAISE method is to translate RSL specifications to Isabelle/HOL and use the theorem prover Isabelle. Institutions and institution representations are used as foundations for the translation. To describe the model-theoretic semantics of RSL, the concept of looser semantics is introduced. An institution for a subset of RSL is presented, higher-order logic is considered, and it is outlined how to translate RSL specifications into Isabelle/HOL.
    Original languageEnglish
    Publication date2002
    Publication statusPublished - 2002
    EventComputer Science and Engineering PhD Day May 2002 -
    Duration: 1 Jan 2002 → …

    Conference

    ConferenceComputer Science and Engineering PhD Day May 2002
    Period01/01/2002 → …

    Bibliographical note

    pp. 45-62
    IMM-TR-2002-8

    Keywords

    • proof support
    • RAISE
    • institutions
    • HOL
    • RSL
    • Isabelle

    OpenUrl availability

    Full text

    Fingerprint

    Dive into the research topics of 'Specify in RSL and Prove in Isabelle'. Together they form a unique fingerprint.
    View full fingerprint

    Cite this