Hoy en día, Android representa más del 80% de la cuota de mercado global. Una tasa tan alta convierte a las aplicaciones de Android en un tema importante que plantea serias preguntas sobre su seguridad, privacidad, comportamiento indebido y corrección. El análisis del código de la aplicación es, sin duda, el medio más apropiado y natural para abordar estos problemas. Sin embargo, ningún análisis podría llevarse a cabo con confianza en ausencia de una sólida base formal. En este documento, proponemos un enfoque formal completo para construir la semántica operativa de una aplicación de Android dada mediante la ingeniería inversa de su código tipo ensamblador, llamado Smali. Llamamos al nuevo lenguaje formal Smali+. Su semántica consiste en dos partes. La primera modela un programa de un solo hilo, en el que se presenta un conjunto de instrucciones principales. La segunda presenta la semántica de un programa multihilo, que es una característica importante en Android que ha sido pasada por alto en los trabajos más avanzados. Todos los elementos esenciales de la multihilo, como la programación, la comunicación entre hilos y la sincronización, se consideran en estas semánticas. La semántica resultante, que forma Smali+, está destinada a proporcionar una base formal para desarrollar técnicas de aplicación de seguridad, análisis y detección de comportamientos indebidos para aplicaciones de Android.