max planck institut
mpii logo Minerva of the Max Planck Society

Download current SPASS Prototypes and Experiments right now!

These pages provide very recent SPASS developments and experiments. More elaborate versions may eventually find their way into the SPASS distribution. In particular, be aware that the offered SPASS binaries my not be robust and documentation is not extensive. However, the SPASS prototype versions will at least perform the offered new functionality on the provided examples.

Generalized Renaming

SPASS(iSAT) on collision avoidance protocols

SPASS(LA) implementing superposition modulo linear arithmetic

Finite Domain Experiments

Authorization Analysis

Disunification and Predicate Completion with SPASS



DHCP Reachability Probability Analysis via FPTA

KBO Constraint Solving