Automatically refining abstract interpretations Abstract interpretation techniques prove properties of programs by computing abstract fixpoints. All such analyses suffer from the possibility of false errors. We present three techniques to automatically refine such abstract interpretations to reduce false errors: (1) a new operator called interpolated widen, which automatically recovers precision lost due to widen, (2) a new way to handle disjunctions that arise due to refinement, and (3) a new refinement algorithm, which refines abstract interpretations that use the join operator to merge abstract states at join points. We have implemented our techniques in a tool Dagger. Our experimental results show our techniques are effective and that their combination is even more effective than any one of them in isolation. We also show that Dagger is able to prove properties of C programs that are beyond current abstraction-refinement tools, such as Slam, Blast, Armc, and our earlier tool.
Keywords for this software
References in zbMATH (referenced in 10 articles )
Showing results 1 to 10 of 10.
- D’Silva, Vijay; Urban, Caterina: Abstract interpretation as automated deduction (2017)
- D’Silva, Vijay; Urban, Caterina: Abstract interpretation as automated deduction (2015)
- Stigge, Martin; Yi, Wang: Combinatorial abstraction refinement for feasibility analysis of static priorities (2015)
- Alkhalid, Abdulaziz; Amin, Talha; Chikalov, Igor; Hussain, Shahid; Moshkov, Mikhail; Zielosko, Beata: Optimization and analysis of decision trees and rules: dynamic programming approach (2013)
- Löwe, Stefan: Cpachecker with explicit-value analysis based on CEGAR and interpolation. (Competition contribution) (2013)
- Gulavani, Bhargav S.; Chakraborty, Supratik; Nori, Aditya V.; Rajamani, Sriram K.: Refining abstract interpretations (2010)
- Gupta, Ashutosh; Popeea, Corneliu; Rybalchenko, Andrey: Non-monotonic refinement of control abstraction for concurrent programs (2010)
- Cousot, Patrick; Cousot, Radhia; Feret, Jér^ome; Mauborgne, Laurent; Miné, Antoine; Rival, Xavier: Why does Astrée scale up? (2009)
- Laviron, Vincent; Logozzo, Francesco: SubPolyhedra: A (more) scalable approach to infer linear inequalities (2009)
- Gulavani, Bhargav S.; Chakraborty, Supratik; Nori, Aditya V.; Rajamani, Sriram K.: Automatically refining abstract interpretations (2008)