		Topic - Security and Accuracy of Information Systems and Communications Team VESONTIO (VESONTIO) Description The goal of this action is to develop formal methods for verifying infinite, parameterized or large systems. We address various verification problems using abstraction techniques based on symbolic representations from various theories: languages and automata, logics, rewriting systems etc. We especially focus on: Communication protocols (secured or not), Communicating systems (automata, process algebraic models, etc.), Security and safety properties (reachability analysis), Quantitative approaches for system verification, Analysis of structured documents (tree automata). We especially give heed to offer tractable algorithmic solutions to these problems.