Predicate Analysis with Block-Abstraction Memoization

D. Wonisch, H. Wehrheim, in: Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM), 2012, pp. 332–347.

Download
Restricted 590-WonischWehrheim2012.pdf 320.90 KB
Conference Paper
Author
;
Abstract
Predicate abstraction is an established technique for reducing the size of the state space during verification. In this paper, we extend predication abstraction with block-abstraction memoization (BAM), which exploits the fact that blocks are often executed several times in a program. The verification can thus benefit from caching the values of previous block analyses and reusing them upon next entry into a block. In addition to function bodies, BAM also performs well for nested loops. To further increase effectiveness, block memoization has been integrated with lazy abstraction adopting a lazy strategy for cache refinement. Together, this achieves significant performance increases: our tool (an implementation within the configurable program analysis framework CPAchecker) has won the Competition on Software Verification 2012 in the category “Overall”.
Publishing Year
Proceedings Title
Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM)
Page
332-347
LibreCat-ID

Cite this

Wonisch D, Wehrheim H. Predicate Analysis with Block-Abstraction Memoization. In: Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM). LNCS. ; 2012:332-347. doi:10.1007/978-3-642-34281-3_24
Wonisch, D., & Wehrheim, H. (2012). Predicate Analysis with Block-Abstraction Memoization. In Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM) (pp. 332–347). https://doi.org/10.1007/978-3-642-34281-3_24
@inproceedings{Wonisch_Wehrheim_2012, series={LNCS}, title={Predicate Analysis with Block-Abstraction Memoization}, DOI={10.1007/978-3-642-34281-3_24}, booktitle={Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM)}, author={Wonisch, Daniel and Wehrheim, Heike}, year={2012}, pages={332–347}, collection={LNCS} }
Wonisch, Daniel, and Heike Wehrheim. “Predicate Analysis with Block-Abstraction Memoization.” In Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM), 332–47. LNCS, 2012. https://doi.org/10.1007/978-3-642-34281-3_24.
D. Wonisch and H. Wehrheim, “Predicate Analysis with Block-Abstraction Memoization,” in Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM), 2012, pp. 332–347.
Wonisch, Daniel, and Heike Wehrheim. “Predicate Analysis with Block-Abstraction Memoization.” Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM), 2012, pp. 332–47, doi:10.1007/978-3-642-34281-3_24.
Main File(s)
File Name
590-WonischWehrheim2012.pdf 320.90 KB
Access Level
Restricted Closed Access
Last Uploaded
2018-03-15T08:33:56Z


Export

Marked Publications

Open Data LibreCat

Search this title in

Google Scholar