The research unit develops new theories, algorithms, and tools for system verification and engineering. We particularly focus on automated reasoning, models of computation, and rigorous systems engineering.