A dataflow analysis to improve SAT-based bounded program verification

SAT-based bounded verification of programs consists of the translation of the code and its annotations into a propositional formula. The formula is then analyzed for specification violations using a SAT-solver. This technique is capable of proving the absence of errors up to a given scope. SAT is a...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Cuervo Parrino, B., Galeotti, J.P., Garbervetsky, D., Frias, M.F.
Formato: SER
Materias:
Bounded program verifications
Empirical evaluations
Logical representations
NP complete problems
Propositional formulas
Propositional variables
SAT solvers
SAT-based bounded verification
Verification tools
Computational complexity
Data flow analysis
Formal logic
Program translators
Verification
Formal methods
Acceso en línea:http://hdl.handle.net/20.500.12110/paper_03029743_v7041LNCS_n_p138_CuervoParrino
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires

Ejemplares similares

Ejemplares similares