Servois is an experimental tool for automatically generating commutativity conditions from data-structure specifications.
Commutativity Condition RefinementKshitij Bansal, Eric Koskinen, Omer Tripp
(conference version under submission)
The source is available on GitHub
https://github.com/kbansal/servois under a BSD license.
- All source code is in the
- In particular,
./src/synth.pyis the implementation of the core algorithm. It needs
cvc4. One may modify the solver variable in the python script to make it point to where it is installed on one's system.
- Input specifications are in
test/subdirectory. They have extensions
cd test; ./runall.pyto run all tests. It prints commands it is running, as well as the commutativity conditions generated.
- Requires CVC4 v1.5 or higher.