Dagger

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.


References in zbMATH (referenced in 13 articles )

Showing results 1 to 13 of 13.
Sorted by year (citations)

  1. D’Silva, Vijay; Urban, Caterina: Abstract interpretation as automated deduction (2017)
  2. Kafle, Bishoksan; Gallagher, John P.: Horn clause verification with convex polyhedral abstraction and tree automata-based refinement (2017)
  3. D’Silva, Vijay; Urban, Caterina: Abstract interpretation as automated deduction (2015)
  4. Stigge, Martin; Yi, Wang: Combinatorial abstraction refinement for feasibility analysis of static priorities (2015)
  5. Alkhalid, Abdulaziz; Amin, Talha; Chikalov, Igor; Hussain, Shahid; Moshkov, Mikhail; Zielosko, Beata: Optimization and analysis of decision trees and rules: dynamic programming approach (2013)
  6. Löwe, Stefan: Cpachecker with explicit-value analysis based on CEGAR and interpolation. (Competition contribution) (2013) ioport
  7. Lee, Woosuk; Lee, Wonchan; Yi, Kwangkeun: Sound non-statistical clustering of static analysis alarms (2012)
  8. Gulavani, Bhargav S.; Chakraborty, Supratik; Nori, Aditya V.; Rajamani, Sriram K.: Refining abstract interpretations (2010)
  9. Gupta, Ashutosh; Popeea, Corneliu; Rybalchenko, Andrey: Non-monotonic refinement of control abstraction for concurrent programs (2010)
  10. Cousot, Patrick; Cousot, Radhia; Feret, Jér^ome; Mauborgne, Laurent; Miné, Antoine; Rival, Xavier: Why does Astrée scale up? (2009)
  11. Heizmann, Matthias; Hoenicke, Jochen; Podelski, Andreas: Refinement of trace abstraction (2009)
  12. Laviron, Vincent; Logozzo, Francesco: SubPolyhedra: A (more) scalable approach to infer linear inequalities (2009)
  13. Gulavani, Bhargav S.; Chakraborty, Supratik; Nori, Aditya V.; Rajamani, Sriram K.: Automatically refining abstract interpretations (2008)