Dissemination
- Workshops
- Past Workshops
- Schools and Seminars
- International Collaboration
- Publications
- Contributions to Standards
- Course Materials Available Online
ARTIST2 PhD Course on: Automated Formal Methods for Embedded Systems
| June 4-12, 2007 DTU - Lyngby, Denmark | organised and funded by ARTIST |
Schedule
Monday, June 4th - Tuesday, June 12th 2007
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 | |
(c) Artist Consortium, All Rights Reserved - 2006, 2007, 2008, 2009