Predicate Abstraction with Minimum Predicates.

摘要: Predicate abstraction is a popular technique employed in formal software verification. A crucial requirement to make predicate effective use as few predicates possible, since the process worst case exponential (in both time and memory requirements) number of involved. If property can be proven hold or not based on given finite set \(\mathcal{P}\), procedure we propose this paper finds automatically minimal subset \(\mathcal{P}\) that sufficient for proof. We explain how our used more efficient verification C programs. Our experiments show minimization result significant reduction usage compared earlier methods.