Generador de condiciones de verificación

Un generador de condiciones de verificación es un subcomponente común de un verificador de programas automatizado que sintetiza condiciones de verificación formales analizando el código fuente de un programa mediante un método basado en la lógica de Hoare . Los generadores de condiciones de verificación pueden requerir que el código fuente contenga anotaciones lógicas proporcionadas por el programador o el compilador, como precondiciones/postcondiciones e invariantes de bucle (una forma de código que contiene pruebas ). Los generadores de condiciones de verificación suelen estar integrados con solucionadores SMT en la parte posterior de un verificador de programas. Una vez que un generador de condiciones de verificación ha creado las condiciones de verificación, estas se pasan a un demostrador de teoremas automatizado , que puede probar formalmente la corrección del código.

Se han propuesto métodos para utilizar la semántica operacional de los lenguajes de máquina para generar automáticamente generadores de condiciones de verificación. ^{[ 1 ]}