Symbolic Abstraction

Symbolic abstraction is a technique that computes the best abstract domain element that overapproximates a given formula in first-order logic.

Symbolic Abstraction in Arlib

Refer to arlib/symabs for the following implementations:

ai_symabs

The implementation from UC Davis’s Automated Reasoning Group. For more details, see Thakur, A. V. (2014, August). Symbolic Abstraction: Algorithms and Applications (Ph.D. dissertation). Computer Sciences Department, University of Wisconsin, Madison.

omt_symabs

The implementation based on OMT solving.

Future Directions

Research Areas

  1. Theory Development: - New abstract domains - Combination methods - Completeness results

  2. Algorithm Improvement:

References

  • Automating Abstract Interpretation, VMCAI’16

  • Program Analysis via Efficient Symbolic Abstraction, OOPSLA’21

  • Thakur, A. V. (2014, August). Symbolic Abstraction: Algorithms and Applications (Ph.D. dissertation). Computer Sciences Department, University of Wisconsin, Madison.