Ausfuehrungssemantik von AutoFocus-Modellen: Isabelle/HOL-Formalisierung und Aequivalenzbeweis

Document type:: Technical Report
Author(s):: David Trachtenherz
Title:: Ausfuehrungssemantik von AutoFocus-Modellen: Isabelle/HOL-Formalisierung und Aequivalenzbeweis
Abstract:: Wir formalisieren den stark kausalen Ausschnitt der Ausfuehrungssemantik des CASE-Werkzeugs AutoFocus in dem Beweisassistenten Isabelle/HOL und zeigen die Aequivalenz dieser Darstellung und der formalen Definition der AutoFocus-Semantik in frueheren Arbeiten und diesem Bericht
Keywords:: AutoFocus; Isabelle/HOL; Formal Semantics; Formal Verification; Theorem Proving
Year:: 2009
Year / month:: 2009-01-23 00:00:00
Pages:: 36
BibTeX

Occurrences: