About Spear — Fast Bit-Vector Arithmetic Theorem Prover
Spear is an industrial strength bit-vector arithmetic (a.k.a modular arithmetic, machine arithmetic) decision procedure and a Boolean satisfiability (SAT) solver. It’s designed for proving software verification conditions, and it’s the main tool Calysto uses for bug hunting. Spear is heavily optimized and tested. Spear supports all standard operators, including multiplication, division, variable shifts, and so on.
Supported Formats
Availability
The tool is freely available for research usage and can be downloaded on the download page. Chances are (95%) that I will eventually open-source Spear and put it in the public domain. If you are interested to continue Spear development and/or using Spear commercially, please drop me an email.
I'm trying to keep Spear up-to-date, as much as I can. Unfortunately, I have very little free time these days and there are several known bugs that I just haven't had time to fix. I apologize for the inconvenience these bugs might be causing you.
Interesting Features
- All search parameters are tunable on the command line.
- Predefined parameter sets for certain types of problems. If you find a set of parameters that works particularly well on a certain set of problems, please let me know, and I’ll add it to the next release.
- Automatic parameter tuning for a specific application with ParamILS tool. See the tools page for details.
- Spear supports all standard modular arithmetic (bitvector) operators, including (un)signed division, remainder, shifting by variable number of spaces,...
Important Notes
- The front-end has been completely rewritten in v2.0, and there has been a number of other modifications. I do expect bugs to pop up, especially since I don’t use that interface for my work (Calysto talks directly to Spear, via API).
- Mac OS X binary is dynamically linked, while all others are linked statically.
- Starting with v2.0, Mac OS X support will be discontinued. It amounts to less than 5% of downloads.
- Certain optimizations in v2.0 won’t work on cyclic expressions. If you can, make sure your expressions are acyclic! For example, instead of:
v 1.0
d a:i1 Tmp1:i1
c Tmp1 ~ a
p = a Tmp1
where Tmp1 is defined in terms of a and a is equal to Tmp1, try rewriting your formulas so as to be acyclic:
v 1.0
d a:i1 Tmp1:i1 Tmp2:i1
c Tmp1 ~ a
p = Tmp2 a
p = Tmp1 Tmp2
If you absolutely need to be able to have cyclic expressions, please send me an email, I'd really like to understand why do you need them. If you disable cse/simplify in Spear, most likely Spear will also swallow your cyclic formulas, but I'm not sure. Thanks to Evgeny Pavlenko for asking a question about this, which motivated me to write this comment.
