Login
- Dokumenttyp:
- Technical Report
- Autor(en):
- Andreas Wolf; Andreas Kmoch
- Titel:
- Einsatz eines automatischen Theorembeweisers in einer taktikgesteuerten Beweisumgebung zur Loesung eines Beispiels aus der Hardware-Verifikation --- Fallstudie ---
- 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.
- Stichworte:
- Automated Theorem Proving; Interactive Theorem Proving; Hardware Verification; Case Study; Proof Tactics
- Jahr:
- 1997
- Jahr / Monat:
- 1997-05-01 00:00:00
- Seiten/Umfang:
- 56
BibTeX