----------
References
----------

The datasets are generated from the application described in the following paper:

On Abstraction Refinement for Program Analyses in Datalog. Xin Zhang, Ravi Mangal, Radu Grigore, Mayur Naik and Hongseok Yang. 
In the proceeding of the 35th annual ACM SIGPLAN conference on Programming Language Design and Implementation, 2014.

-----------
Application
-----------

The submitted MaxSAT instances solve the problem of finding an optimum abstraction for a program analysis. Program abstraction
controls the scalability and precision of a given analysis. It is a central tasks in program analysis to choose an abstraction
that strikes a balance between these two metrics. The referred paper applies a lazy approach which iteratively invokes a MaxSAT
solver to find an optimum abstraction for an analysis on a given program.

--------
Datasets
--------

All the instances are weighted partial MaxSAT instances.

The datasets are generated by applying the described approach on a polymorphic call site analysis and a downcast safety checker.
The former concerns the question whether an virtual method call in a Java program might invoke different methods at runtime,
whether the latter concerns whether a downcast can fail at runtime. We applied the approach on six programs and took one instance
from each run. The programs are as follows:

lusearch: text search tool.

bloat: bytecode optimization/analysis tool.

pmd: Java source analyzer.

avrora: microcontroller simulator/analyzer.

hsqldb: SQL relational database engine.

xalan: XSLT processor to transform XML.

--------
Contacts
--------

Xin Zhang, xin.zhang@gatech.edu
Xujie Si, six@gatech.edu
Mayur Naik, naik@cc.gatech.edu