TU Wien:Computer Aided Verification VU (Veith)/Prüfung 28.6.2013
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)