Biabduction solver for Symbolic Heap Separation Logic with Arrays and Lists

[Contents]

build.sh : build script of biabdAL
src/ : source files of biabdAL
testfiles/ : example input files (handwritten)
slactestfiles/ : experimental files for SLAC

[Requirements for build biabdAL]
- make
- opam (OCaml, ocamlopt, ocamlyacc, ocamllex, ocamlfind, z3-package, ANSITerminal-package)

[Build]
./build.sh

[Usage]
./biabdAL -f FILE [-balimit NUM|-nooutput|-debug]

[Options]
-balimit NUM : set limit number of iteration (default: -1 (nolimit))
-nooutput : avoid showing solutions (only shows the number of solutions)
-debug : show detailed outputs