Un generador de condiciones de verificación es un subcomponente común de un verificador de programas automatizado que sintetiza las condiciones de verificación formales mediante el análisis del código fuente de un programa utilizando un método basado en la lógica de Hoare . Los generadores de VC pueden requerir que el código fuente contenga anotaciones lógicas proporcionadas por el programador o el compilador, como condiciones previas / posteriores e invariantes de bucle (una forma de código de prueba ). Los generadores de VC a menudo se combinan con solucionadores SMT en el backend de un verificador de programas. Después de que un generador de condiciones de verificación ha creado las condiciones de verificación, se pasan a un comprobador de teoremas automatizado., que luego puede probar formalmente la exactitud del código.
Se han propuesto métodos para utilizar la semántica operativa de los lenguajes de máquina para generar automáticamente generadores de condiciones de verificación. [1]
Referencias
- ^ John Matthews; J. Strother Moore ; Sandip Ray; Daron Vroon (2005). "Generación de la condición de verificación a través de la demostración del teorema" . En Miki Hermann; Andrei Voronkov (eds.). Proc. En t. Conf. Lógica para programación, inteligencia artificial y razonamiento . LNCS. 4246 . Saltador. págs. 362–376.