Abstract counterexample-based refinement for powerset domains

R. Manevich, J. Field, T.A. Henzinger, G. Ramalingam, M. Sagiv, in:, Program Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday, Springer, 2007, pp. 273–292.

Download
No fulltext has been uploaded. References only!

Book Chapter | Published
Author
; ; ; ;
Series Title
LNCS
Abstract
Counterexample-guided abstraction refinement (CEGAR) is a powerful technique to scale automatic program analysis techniques to large programs. However, so far it has been used primarily for model checking in the context of predicate abstraction. We formalize CEGAR for general powerset domains. If a spurious abstract counterexample needs to be removed through abstraction refinement, there are often several choices, such as which program location(s) to refine, which abstract domain(s) to use at different locations, and which abstract values to compute. We define several plausible preference orderings on abstraction refinements, such as refining as “late” as possible and as “coarse” as possible. We present generic algorithms for finding refinements that are optimal with respect to the different preference orderings. We also compare the different orderings with respect to desirable properties, including the property if locally optimal refinements compose to a global optimum. Finally, we point out some difficulties with CEGAR for non-powerset domains.
Publishing Year
Date Published
2007-03-30
Book Title
Program Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday
Acknowledgement
This research is partially supported by the Clore Fellowship Programme. Supported in part by the Swiss National Science Foundation.
Volume
4444
Page
273 - 292
IST-REx-ID

Cite this

Manevich R, Field J, Henzinger TA, Ramalingam G, Sagiv M. Abstract counterexample-based refinement for powerset domains. In: Program Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday. Vol 4444. Springer; 2007:273-292. doi:10.1007/978-3-540-71322-7_13
Manevich, R., Field, J., Henzinger, T. A., Ramalingam, G., & Sagiv, M. (2007). Abstract counterexample-based refinement for powerset domains. In Program Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday (Vol. 4444, pp. 273–292). Springer. https://doi.org/10.1007/978-3-540-71322-7_13
Manevich, Roman, John Field, Thomas A Henzinger, Ganesan Ramalingam, and Mooly Sagiv. “Abstract Counterexample-Based Refinement for Powerset Domains.” In Program Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday, 4444:273–92. Springer, 2007. https://doi.org/10.1007/978-3-540-71322-7_13.
R. Manevich, J. Field, T. A. Henzinger, G. Ramalingam, and M. Sagiv, “Abstract counterexample-based refinement for powerset domains,” in Program Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday, vol. 4444, Springer, 2007, pp. 273–292.
Manevich R, Field J, Henzinger TA, Ramalingam G, Sagiv M. 2007. Abstract counterexample-based refinement for powerset domains. Program Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday. , LNCS, vol. 4444. 273–292.
Manevich, Roman, et al. “Abstract Counterexample-Based Refinement for Powerset Domains.” Program Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday, vol. 4444, Springer, 2007, pp. 273–92, doi:10.1007/978-3-540-71322-7_13.

Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar