Welcome to the home page of the
Succinct Solver. The succinct solver is a tool for solving constrains specified
by the Alternation-free Least Fixed Point Logic (ALFP) in clausal form, which is
an extension of Horn Clause. The succinct solver is developed cooperatively by the group of
Safe and Secure IT Systems
at the
Informatics and Mathematical Modelling
department, Technical University of Denmark and the group of
Program Languages and Compilers
, at the
Computer Science
department, University of Trier.
The Succinct Solver has been
evolved from the earlier version (V1.0) which is based on the bounded finite
universe that can be pre-computed directly from the clause of interest, to the
extended version (V2.0) which considers unbounded universe that is dynamically
expanded with the solving process. Both versions can be downloaded from the
download page. For
more information, please refer to the companion
documents.
The Succinct Solver is a free
tool for researchers and developers subject to the
license.