Cadence Berkeley Labs.

@misc{citeulike:3090643, abstract = {The success of model checking for large programs depends crucially on the ability to efficiently construct parsimonious abstractions. A predicate abstraction is parsimonious if at each control location, it specifies only relationships between current values of variables, and only those which are required for proving correctness. Previous methods for automatically refining predicate abstractions until sufficient precision is obtained do not systematically construct parsimonious abstractions: predicates usually contain symbolic variables, and are added heuristically and often uniformly to many or all control locations at once. We use Craig interpolation to efficiently construct, from a given abstract error trace which cannot be concretized, a parsominous abstraction that removes the trace. At each location of the trace, we infer the relevant predicates as an interpolant between the two formulas that define}, author = {Henzinger, Thomas A. and Jhala, Ranjit and Majumdar, Rupak and Mcmillan, Kenneth L. }, citeulike-article-id = {3090643}, keywords = {abstraction, model\_checking}, posted-at = {2008-08-06 13:01:58}, priority = {4}, title = {Cadence Berkeley Labs.}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.1200} }

TY - ELEC ID - citeulike:3090643 L3 - citeulike-article-id:3090643 TI - Cadence Berkeley Labs. N2 - The success of model checking for large programs depends crucially on the ability to efficiently construct parsimonious abstractions. A predicate abstraction is parsimonious if at each control location, it specifies only relationships between current values of variables, and only those which are required for proving correctness. Previous methods for automatically refining predicate abstractions until sufficient precision is obtained do not systematically construct parsimonious abstractions: predicates usually contain symbolic variables, and are added heuristically and often uniformly to many or all control locations at once. We use Craig interpolation to efficiently construct, from a given abstract error trace which cannot be concretized, a parsominous abstraction that removes the trace. At each location of the trace, we infer the relevant predicates as an interpolant between the two formulas that define KW - abstraction KW - model_checking AU - Henzinger, Thomas AU - Jhala, Ranjit AU - Majumdar, Rupak AU - Mcmillan, Kenneth UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.1200 ER -