Verification and falsification of programs with loops using predicate abstraction.

Predicate abstraction is amajor abstraction technique for the verification of software.Data is abstracted by means of Boolean variables, which keep track of predicates over the data. In many cases, predicate abstraction suffers from the need for at least one predicate for each iteration of a loop co...

Description complète

Détails bibliographiques
Auteurs principaux: Kroening, D, Weissenbacher, G
Format: Journal article
Langue:English
Publié: 2010