ARTIST2 PhD Course on: Automated Formal Methods for Embedded Systems

June 4-12, 2007       DTU - Lyngby, Denmark organised and funded by ARTIST 


Monday, June 4th - Tuesday, June 12th 2007


Morning Introduction to the course, modeling of finite-state systems
Afternoon Computation tree logic (CTL) and CTL model checking


--- 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


Morning Modular Performance Analysis with Real Time Calculus
Afternoon Hands-on exercises with RTC


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

Réalisation Axome - Création de sites Internet