Abstract
Los sistemas embebidos son fundamentales en la tecnología actual, y el lenguaje C es ampliamente utilizado para su programación. No obstante, los errores en C suelen ser difíciles de detectar con pruebas convencionales debido a su naturaleza sutil y efectos impredecibles. Para mejorar la confiabilidad del software embebido, este trabajo propone una estrategia que combina la programación por contratos y la verificación estática con VeriFast. El enfoque se aplica a dos casos de código en C, con especial énfasis en software crítico, como drivers en arquitecturas por capas, donde los fallos en producción pueden generar pérdidas significativas. La metodología propuesta contribuye a sistematizar las pruebas de correctitud y mejorar la confiabilidad del software embebido.