IEEE/ICACT20220362 Slide.15
[Big Slide]
[YouTube] Oral Presentation 
| Virual Oral Presentation Slide by Slide |
|
IEEE/ICACT20220362 Slide.15
[Big Slide]
[YouTube] |
Oral Presentation |
|
|
|
Liveness properties are based on the concept that ˇ°something will eventually happen.ˇ± We verified ˇ°A<> not(sw1.out_port && sw1.drop)ˇ± The figure is also verification results for ˇ°Property is satisfied.ˇ± This means that a packet P on all path could not go out_port and drop locations of Switch 1 in order to liveness property. | |
| [Go to Next Slide] |