Einsatz eines automatischen Theorembeweisers in einer taktikgesteuerten Beweisumgebung zur Loesung eines Beispiels aus der Hardware-Verifikation --- Fallstudie ---

Title:: Einsatz eines automatischen Theorembeweisers in einer taktikgesteuerten Beweisumgebung zur Loesung eines Beispiels aus der Hardware-Verifikation --- Fallstudie ---
Document type:: Technical Report
Author(s):: Andreas Wolf; Andreas Kmoch
Abstract:: Anhand einer Fallstudie aus dem Bereich der Verifikation eines Mikroprozessors wird der Einsatz des automatischen Theorembeweisers SETHEO in einer interaktiven taktikgesteuerten Beweisumgebung demonstriert. Dazu wird nach Vorstellung der theoretischen Grundlagen beschrieben, wie dieser Einsatz erfolgt. Es werden die verwendeten Taktiken erl"autert und die maschinell generierten Beweise angegeben.
Keywords:: Automated Theorem Proving; Interactive Theorem Proving; Hardware Verification; Case Study; Proof Tactics
Year:: 1997
Year / month:: 1997-05-01 00:00:00
Pages:: 56
BibTeX

Occurrences: