Example-Guided Abstraction Simplification

Guided Abstraction Simplification Roberto Giacobazzi1 and Francesco Ranzato2 1 University of Verona, Italy 2 University of Padova, Italy Abstract. In static analysis, approximation is typically encoded by abstract domains, providing systematic guidelines for specifying approximate semantic functions and precision assessments. However, it may well happen that an abstract domain contains redundant information for the specific purpose of approximating a given semantic function modeling some behavior of a system. This paper introample-Guided Abstraction Simplification (EGAS), a methodology for simplifying abstract domains, i.e. removing abstract values from them, in a maximal way while retaining exactly the same approximate behavior of the system unysis. We show that, in abstract model checking and predicate abstraction, vides a simplification paradigm of the abstract state space that is guided les, meaning that it preserves spuriousness of examples (i.e., abstract paths). In particular, w...

• Type: Conference
• Year: 2010
• Where: ICALP
• Authors: Roberto Giacobazzi, Francesco Ranzato
• Keywords: Abstract Domains, Abstraction Simplification, Abstraction Simplification Roberto, ICALP 2010, Programming Languages