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.