 |
|
 |
|
Nichtsequentielle Systeme und nebenläufige Prozesse
|
|
|
|
|
 |
|
held by: |
Univ.-Prof. Dr. Helmut Veith †
|
|
|
held in: |
SS 2005
|
|
|
schedule: |
Wednesday, 08:30 - 11:00 (MI HS1) start date: 2005-04-20 / end date: 2005-07-13
Thursday, 12:00 - 14:00 (MW0250) start date: 2005-04-21 / end date: 2005-07-14
|
|
|
sws: |
4
|
|
|
Have a look at our OBDD Workbench! |
|
|
downloadable material:
|
|
|
slides
|
title / description
|
download
|
|
Temporal Logic Model Checking
|
click here...
|
|
Binary Decision Diagrams
|
click here...
|
|
Basic Fix Point Theorems
|
click here...
|
|
Symbolic Model Checking
|
click here...
|
|
SMV
|
click here...
|
|
Abstraction
|
click here...
|
|
Bounded Model Checking
|
click here...
|
|
Partial Order Reduction
|
click here...
|
|
SPIN Example: Peterson's Algorithm
|
click here...
|
|
SPIN Notes
|
click here...
|
|
|
|
other
|
title / description
|
download
|
|
Temporal Model Checking
|
click here...
|
|
Progress on the State Explosion Problem in Model Checking
|
click here...
|
|
SMV Examples
|
click here...
|
|
Promela Examples
|
click here...
|
|
Promela Examples II
|
click here...
|
|
|
 |
|
|
 |