Symbolic Implementation of the Best Transformer

This paper shows how to achieve, under certain conditions, abstract-interpretation ms that enjoy the best possible precision for a given abstraction. The key idea is a simple process of successive approximation that makes repeated calls to a decision proced obtains the best abstract value for a set of concrete stores that are represented symbolically, using a logical formula.

• Type: Conference
• Year: 2004
• Where: VMCAI
• Authors: Thomas W. Reps, Shmuel Sagiv, Greta Yorsh
• Keywords: Abstract-interpretation Ms, Certain Conditions, Software Engineering, Successive Approximation, VMCAI 2004