Servois is an experimental tool for automatically generating commutativity conditions from data-structure specifications.
Automatic Generation of Precise and Useful Commutativity ConditionsKshitij Bansal, Eric Koskinen, Omer Tripp
(to appear) In Proceedings of TACAS, 2018.
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.