They are boolean abstraction of asynchronous programs obtained from SATABS which were then converted to NTS. To make the NTS recursionless a bounded index approximation was applied on the boolean abstracted asynchronous program. The unbounded variables in the NTS encode the buffer of pending tasks. Those examples have been produced by an OCAML prototype implemented by Bishesh Adhikari during an internship at the IMDEA Software Institute.
They are underapproximations of asynchronous programs with integer variables
obtained by applying the delay-bounded
scheduling underpproximation of
Emmi, Qadeer and Rakamaric which returns a recursive sequential programs over
integer variables. The input programs are defined in the
boogie language whereas
the ouput programs are defined as NTS. We adapted the
tool c2s of Michael Emmi to ouput the NTS
programs. Those recursive sequential NTS programs are located in the dbseq/x.y/ directory.
Because some tools do not handle recursion we further applied an index-bounded
underapproximation on these
programs. The resulting recursionless sequential NTS programs are located in
the x.y/z subdirectories.