Model Checking

Wintersemester

Inhalte

• Transitionssysteme
• LTL (Linear temporal logic)
• Büchiautomaten
• CTL (Computation tree logic)
• Ordered Binary Decision Diagrams und symbolisches Model-Checking
• Pushdownsysteme und Model-Checking rekursiver Programme