TacoFlow: optimizing SAT program verification using dataflow analysis

In previous work, we presented TACO, a tool for efficient bounded verification. TACO translates programs annotated with contracts to a SAT problem which is then solved resorting to off-the-shelf SAT-solvers. TACO may deem propositional variables used in the description of a program initial states as...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Cuervo Parrino, B., Galeotti, J.P., Garbervetsky, D., Frias, M.F.
Formato: JOUR
Materias:
Dataflow analysis
Java-like programs verification
SAT-based verification
Boolean functions
Computer software
Formal logic
Java programming language
Bounded verifications
Empirical evaluations
Java-like programs
Levels of abstraction
Program Verification
Propositional variables
SAT-based
Worst-case complexity
Data flow analysis
Acceso en línea:http://hdl.handle.net/20.500.12110/paper_16191366_v14_n1_p45_CuervoParrino
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires

Ejemplares similares

Ejemplares similares