(1) Una herramienta de software que acepta como entrada un programa informático y una representación de su especificación y produce, posiblemente con ayuda humana, una prueba o refutación de la exactitud de la program.~(2) cualquier herramienta de software que automatiza la parte o la totalidad del proceso de verificación.