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
- Here are the translations of 526 TPTP 5.4.0 formula problem files
(genrenaming.tgz, 2400KB) where
generalized renaming achieves a reduction of at least 5% in the number
of clauses compared to standard renaming.
SPASS(iSAT) on collision avoidance protocols
- TGZ archive (colprot.tgz, 550KB), including
all collision avoidance protocol experiments: input files as well as SPASS(iSAT) output files.
SPASS(LA) implementing superposition modulo linear arithmetic
- PC Linux binary (SPASSLA.tgz, 0.6MB), including
examples. The approach is based on the
hierarchic theorem proving
result by Bachmair, Ganzinger and Waldmann.
Linear arithmetic constraint solving is performed via LP solving using
QSopt. The package contains example
problems formalizing properties of transition systems that can then be automatically proved by SPASS(LA).
From the example files the extended SPASS syntax for linear arithmetic expressions can be easily derived.
Please note that this SPASS(LA) version will crash when applied to non-linear problems and does not support
equational reasoning. This will be fixed and added soon, respectively. SPASS(LA) will be contained in the
next major release of SPASS.
Finite Domain Experiments
- Here is a finite domain problem (LAN-FinDom.cnf)
in SPASS dfg as well as in tptp syntax (LAN-FinDom.tptp).
The problem formalizes part of the LAN infrastructure including Layer 3 IP addressing, router forwarding and
stateful firewalling.
It is satisfiable in a finite domain that in particular includes all 32 Bit IP addresses represented by
32 Bit bitvectors. Its a challenge problem
for any prover targetting satisfiable finite domain problems, in particular if the prover is based on domain
element instantiation.
Authorization Analysis
- The dfg file(sap.dfg, 0.45KB) includes a first-order
theory representing the formalization of an SAP R/3 authorization and process setup together with business
policies for a purchase process.
(SAP and SAP R/3 are registered trademarks of SAP AG in Germany and other countries.)
Disunification and Predicate Completion with SPASS
SPASS-Y2
SPASS-YAGO++
- SPASS-YAGO++ 64-Bit Linux binaries plus all example files including
the YAGO++ ontology ( Yago++.cnf.gz, 248MB) and its finite
saturation ( Yago++.cnf.model.gz, 252MB), as well as
the queries ( Yago++-queries.tgz, 693B).
The SPASS-YAGO++ binary (SPASS-YAGO++.gz, 359KB).
The dfg2tptp binary can be loaded from the SPASS-YAGO distribution above.
For saturation call "SPASS-YAGO++ Yago++.cnf" and for a query the two successive commands
"SPASS-YAGO++ Yago++.cnf.model -Server &" and "cat query.dfg > SYFIFOIN".
DHCP Reachability Probability Analysis via FPTA
- First-order probabilistic timed automata (FPTA) are a generalization of probabilistic timed
automata (PTA) with first-order theories. The archive
(dhcp.tgz 4kB)
contains the FOL(LA) theory of an FPTA describing DHCP,
the MoDeST code of the
generated VPTA out of the reachability proofs for the DHCP bound state,
analyzed by mcpta,
and the resulting PRISM
model for the eventual reachability probability analysis.
KBO Constraint Solving
- We provide experiments for our KBO constraint solver called as a
subprocedure of conguence closure algorithm with variables.
(testsuite.tar.gz 3MB).
