Monday
|
Morning |
Introduction to the course, modeling of finite-state systems |
Afternoon |
Computation tree logic (CTL) and CTL model checking |
|
|
Tuesday
|
--- Public holiday --- |
Wednesday- Symbolic methods I: Finite state
|
Morning |
Circuit equivalence and propositional SAT solving |
Afternoon |
Symbolic representation of transition systems, reachability |
(both bounded and full), symbolic CTL model checking |
Thursday - Symbolic methods II: Hybrid state
|
Morning |
Hybrid discrete-continuous automata models |
Afternoon: |
Verification by approximation |
|
|
Friday - Symbolic techniques III: Satisfiability for large arithmetic formulae
|
Morning |
SAT modulo theory |
Afternoon |
Robust semantics of arithmetic formulae, satisfiability procedures for undecidable arithmetic |
|
|
Monday
|
Morning |
Modular Performance Analysis with Real Time Calculus |
Afternoon |
Hands-on exercises with RTC |
|
|
Tuesday
|
Morning |
Symbolic Timing Analysis for Systems (SymTA/S), a system-level performance and timing analysis approach based on formal scheduling analysis techniques and symbolic simulation |
Afternoon |
Hands-on exercises with SymTA/S |