The research theme of AFM at ICE-ROSE laboratory is mainly to investigate and apply formal methods in developing reactive and concurrent systems. The ongoing research is in the fields of basic theories, practical applications, and developing specialized tools for certain applications. Actor-based models and coordination languages are studied and used in modeling concurrent systems. Formal verification approaches: compositional verification, model checking, reduction techniques for model checking (abstraction, symmetry, partial order reduction) are investigated and applied. The computational models of different application domains including network protocols, Web services, and system-level designs are investigated.