¿Por qué podemos demostrar matemáticamente que un programa no tiene ningún bug sin ejecutarlo ni una sola vez? La ciencia de la verificación formal
