TU Wien:Computer Aided Verification VU (Veith)/Prüfung 28.6.2013

Aus VoWi
Zur Navigation springen Zur Suche springen

Beispiel 1 und 2 gleich wie letztes Jahr.

Beispiel 3 (ungefähr): 5 Variablen, Integer 32 Bit a) Wieviel Bit braucht man in SMV für den Status b) Wieviel Variablen für BDD bei einer Abstraktion h. h(0)=0, h(n)=1 otherwise c) Wieviel Bit für die Transition relation d) vergessen

Beispiel 4 Wieder t/f Fragen.

  • ) Bounded Model Checking kann verwendet werden um das größte Counter Example zu finden. (Finite Kripke Structure)