Two classical sources of imprecision in static analysis by abstract interpretation are widening and merge operations. Merge operations can be done away by distinguishing paths, as in trace partitioning, at the expense of enumerating an exponential number of paths. In this article, we describe how to avoid such systematic exploration by focusing on a single path at a time, designated by SMT-solving. Our method combines well with acceleration techniques, thus doing away with widenings as well in some cases. We illustrate it over the well-known domain of convex polyhedra. © 2011 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Monniaux, D., & Gonnord, L. (2011). Using bounded model checking to focus fixpoint iterations. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6887 LNCS, pp. 369–385). https://doi.org/10.1007/978-3-642-23702-7_27
Mendeley helps you to discover research relevant for your work.