Better Under-Approximation of Programs by Hiding Variables

Abstraction frameworks use under-approximating transitions in order to prove existential properties of concrete systems. Under-approximating transifer to the concrete states that correspond to a particular abstract state in a l manner. For example, there is a must transition from abstract state a to state a only if all the concrete states in a have successors in a . The universal nature of under-approximating transitions makes them closed under transitivity. Consequently, reachability queries about the concrete system, which have applications in falsification and testing, can be answered by reasoning about raction. On the negative side, the universal nature of under-approximating transitions makes them dependent on all the variables of the program. The abstraction, on the other hand, often hides some of the variables. Since the universal quantification in must transitions ranges over all variables, this often prevents the ion from associating a must transition with statements that re...

• Type: Conference
• Year: 2007
• Where: VMCAI
• Authors: Thomas Ball, Orna Kupferman
• Keywords: Concrete States, Partitioned-must Transitions, Software Engineering, Under-approximating Transitions, VMCAI 2007