Paper accepted @ FM 2019 – APML: An Architecture Proof Modeling Language

In this paper, accepted for presentation at the 23rd International Symposium on Formal Methods, we introduce APML, a sound and complete language to sketch proofs for composition of FACTum contracts in a notation similar to Message Sequence Charts. Moreover, we provide an algorithm to generate Isabelle/Isar proofs out of an APML sketch.

The language is implemented in FACTum Studio which supports the user in the development of correct APML proofs. In addition we also implemented the algorithm in FACTum Studio which allows a user to generate Isabelle/Isar proofs out of an APML sketch.

Kommentar verfassen

Trage deine Daten unten ein oder klicke ein Icon um dich einzuloggen:

Du kommentierst mit Deinem Abmelden /  Ändern )

Google Foto

Du kommentierst mit Deinem Google-Konto. Abmelden /  Ändern )


Du kommentierst mit Deinem Twitter-Konto. Abmelden /  Ändern )


Du kommentierst mit Deinem Facebook-Konto. Abmelden /  Ändern )

Verbinde mit %s