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

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. <br>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).<br>The dataset includes .dylib (dynamic library) and .so (shared library files, and the example folder includes .ada (ADA source code). <br>A README file ("Instructions.txt") is also included with instructions to allow replication of the results of the second algorithm.