El software integrado tiene propiedades dependientes del hardware (operación directa de espacios de direcciones, E/S mapeada en memoria, interrupción, etc.). Por lo tanto, las demandas sobre el método establecido de verificaciones formales correspondientes a esas propiedades están aumentando desde el punto de vista de un desarrollo más corto y una alta fiabilidad. Nuestro estudio tiene como objetivo habilitar una verificación formal con Comprobación de Modelo Acotado Basada en Teorías de Satisfacibilidad (SMT-Based BMC) de seguridad para códigos de ensamblaje integrados. Nuestro método propuesto genera modelos de códigos de ensamblaje en detalle con la teoría de vectores de bits de tamaño fijo. Los modelos generados por nuestro método incluyen interrupciones, y el tamaño de los modelos se reduce utilizando la técnica de Reducción de Ejecuciones de Controlador de Interrupciones (IHER). En este documento, hemos desarrollado el método de verificación de propiedades de seguridad de un programa de ensamblaje integrado combinando la Comprobación de Modelo Acotado Basada en SMT y la Reducción de Ejecuciones de Controlador de Interrupciones. Además, mostramos la evaluación de nuestro método mediante experimentos utilizando un verificador de modelos prototipo.