formal verification of finite and infinite state reactive systems
synchronous languages and hardware design
worst-case execution time analysis
symbolic (bounded) model checking and temporal logics
decidable predicate logics and finite automata
processor architectures
