Skip to content

CrabPapers

Jump to bottom
Jorge Navas edited this page Nov 12, 2021 · 11 revisions

Papers explaining the theory behind Crab Implementation

  • The implementation of functional maps (domains/patricia_trees.hpp) is based on "Fast Mergeable Integer Maps" PDF.

    Functional maps are used in all the non-relational domains. They play a major role in the efficiency of binary operations such as join, meet, widening and narrowing.

  • The computation of weak topological orderings (iterators/wto.hpp). "Efficient chaotic iteration strategies with widenings" (PDF) by F. Bourdoncle. The paper describes a recursive algorithm. We implemented a non-recursive version to avoid stack overflows.

  • The fixpoint algorithm (iterators/interleaved_fixpoint_iterator.hpp). "Localizing widening and narrowing" (PDF) by G. Amato and F. Scozzari.

  • This is the paper for the zones domain (domains/split_dbm.hpp). "Exploiting Sparsity in Difference-Bounds Matrices" (PDF) by G. Gange, J. A. Navas, P. Schachte, H. Sondergaard, and P. Stuckey. SAS'16.

  • This is the paper for the octagons domain (domains/split_soct.hpp). "A Fresh Look at Zones and Octagons" (PDF) by G. Gange, J. A. Navas, P. Schachte, H. Sondergaard, and P. Stuckey. In TOPLAS Volume 43, Issue 3 September 2021.

  • This is the paper for the terms domain (domains/term_equiv.hpp). "An Abstract Domain of Uninterpreted Functions" (PDF) by G. Gange, J. A. Navas, P. Schachte, H. Sondergaard, and P. Stuckey. VMCAI'16.

  • This is the paper for the wrapped interval domain (domains/wrapped_interval_domain.hpp). "Signedness-Agnostic Program Analysis: Precise Integer Bounds for Low-Level Code" (PDF) by J. A. Navas, P. Schachte, H. Sondergaard, and P. Stuckey. APLAS'12.

  • This is the paper for the Boxes domain (domains/boxes.hpp). "Boxes: A Symbolic Abstract Domain of Boxes" (PDF) by A. Gurfinkel and S. Chaki. SAS'10.

  • For the constant and sign domains (domains/sign_domain.hpp and domains/constant_domain.hpp), I recommend to look at this tutorial.

  • This is the paper for the congruence domain (domains/congruences.hpp). "Static Analysis of Arithmetical Congruences" (PDF)

  • A new look at widening. "Dissecting Widening: Separating Termination from Information" (PDF) by G. Gange, J. A. Navas, P. Schachte, H. Sondergaard, and P. Stuckey. APLAS'19.

  • The refining forward+backward analyzer is described by Cousot and Cousot in these two papers: JLP'92 and ASE'99 (section 4).

  • For the top-down interprocedural analysis the closest reference I think it would be this.

  • The paper "Abstract Interpretation of LLVM with a Region-Based Memory Model" by A.Gurfinkel and J. A. Navas (PDF) that describes CrabIR, the Crab Intermediate Representation.

Clone this wiki locally