Abstract
Predicate abstraction is an automatic technique that can be used to find abstract models of large or infinite-state systems. In tools like SLAM, where predicate abstraction is applied to software model checking, a number of heuristic approximations must be used to improve the performance of computing an abstraction from a set of predicates. For this reason, SLAM can sometimes reach a state in which it is not able to further refine the abstraction. In this paper we report on an application of Das & Dill's algorithm for predicate abstraction refinement. SLAM now uses this strategy lazily to recover precision in cases where the abstractions generated are too coarse. We describe how we have extended Das & Dill's original algorithm for use in software model checking. Our extension supports procedures, threads, and potential pointer aliasing. We also present results from experiments with SLAM on device driver sources from the Windows operating system. © Springer-Verlag 2004.
Cite
CITATION STYLE
Ball, T., Cook, B., Das, S., & Rajamani, S. K. (2004). Refining approximations in software predicate abstraction. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2988, 388–403. https://doi.org/10.1007/978-3-540-24730-2_30
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
