Artifact related to Abstraction Refinement for Emptiness Checking of Alternating Data Automata (TACAS 2018 paper)

<div>This dataset is associated with a published paper which presented a new model of alternating automata over infinite alphabets. This involved the development of two semi-algorithms inspired by two state-of the-art abstraction refinement model checking methods, lazy predicate abstraction and the Impact semi-algorithm. </div><div><br></div><div>The algorithms were implemented in a prototype tool using the Math-SAT5 SMT solver via the Java SMT interface for the satisfiability queries and interpolant generation, in the theory of linear integer arithmetic with uninterpreted Boolean functions (UFLIA).</div><div><br></div><div>The dataset includes .dylib (dynamic library) and .so (shared library files, and the example folder includes .ada (ADA source code). </div><div><br></div><div>A README file ("Instructions.txt") is also included with instructions to allow replication of the results of the second algorithm.