Verification is a collection of techniques to explore the behaviors of open discrete-event dynamical systems and check whether they satisfy some temporal properties. Its major application domains are software and hardware protocols modeled as automata. The research on timed and hybrid systems attempts to export these concepts toward richer models that include "real" metric time as well as continuous dynamics defined by differential equations. The course will consists of a series of informal presentation of various research threads and results in this domain.

Topics include:

• Verification for dummies
• Reachability computation for continuous and hybrid systems
• Timed automata: fighting the clock explosion
• A unified approach for optimal and reasonable control synthesis
• Optimal scheduling under uncertainty
• Monitoring temporal properties of dense-time real-valued signals
• Learning Omega-automata from examples
• Multi-criteria optimization
• Optimal deployment on multi-cores
• Systems Biology
• Probabilistic decision graphs

This is a visiting professor course of Vienna PhD School of informatics for Computer Engineering. Lecturer: Dr. Oded Maler (VERIMAG, France)

Registration takes place in TISS