Desarrollamos herramientas para el análisis y verificación de propiedades de seguridad (safety) y protección (security) en código móvil (por ejemplo Java o Python), en protocolos de comunicaciones criptográficos, por ejemplo basados en curvas elípticas o criptografía postcuántica, o en sistemas software genéricos, por ejemplo mala gestión de recursos compartidos. El beneficio que aporta VRAIN de la UPV en este sentido es haber desarrollado técnicas avanzadas de reducción del espacio de búsqueda de soluciones que han sido integradas en diferentes aplicaciones desarrolladas en centros de investigación de todo el mundo.