Certificate-producing OpenSMT2

 
This work presents a system for witnessing the unsatisfiability of instances of NP problems, commonly appearing in verification, in a way that is natural to SMT solving. Our implementation of the system seems to often result in significantly smaller witnesses, lower solving overhead, and faster checking time in comparison to existing proof formats that can serve a similar purpose.
 

Docker Image:

A docker image is provided to run the instrumented solver and the checker, you can download it using the following link: Download

Docker Image Guidelines:

Load the image from the downloaded tar archive using the command:

docker image load -i tswc-dac21.tar.gz

You can simply run an interactive shell container using that image and explore image content using the command: 

docker run -it tswc-dac21 bash

To execute the instrumented solver: use "opensmt file", with "file" being the path to the smt2 instance. All certificates will be generated in the ./proof folder, located in the folder from which the call is made.

To execute the checker: use "./tswc certificatesFolder checkerModulesFolder theory", with "certificatesFolder" being the path to the ./proof folder containing the generated certificates, "checkerModulesFolder" being  the path to the folder containing the checker modules, and "theory" being one of "QF_LRA", "QF_LIA", and "QF_UF".
 
Example: the commands 
cd example
 
opensmt bignum_lra2.smt2
 
../tswc.sh ./proof ../modules QF_LRA

terminates with the message "verified - all certificates are valid" and all certificates being stored in the "example/proof" folder.

 
N.B.: If you want to execute the instrumented solver and checker on a local [smt2-instance]: first create your [instance-folder] in the root using an interactive shell, then, on a second shell, get the [container-id] using 
docker ps

and copy [smt2-instance] to the  [instance-folder] using 

docker cp [smt2-instance] [container-id]:/home/[instance-folder]/[smt2-instance]

and finally use "cd [instance-folder]; opensmt [smt2-instance];  ../tswc.sh ./proof ../modules [Theory]" to generate your certificates.

**All certificates being stored in [instance-folder]/proof.
 
Software license agreement
Please read this agreement carefully.
 
Copyright 2021 Formal Verification and Security Lab - USI Lugano 
Permission is hereby granted, free of charge, to any academic user obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software for the purpose of benchmarking it against other tools for SMT solving and model checking, including without limitation the rights to use, copy and distribute, but excluding the right to sell copies of the Software or to exploit it for commercial use, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
 
The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. 
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
To obtain a commercial license contact this email verificationlab@usi.ch

References

  1. Theory-Specific Proof Steps Witnessing Correctness of SMT Executions Otoni, Rodrigo, Blicha Martin, Eugster Patrick, Hyvärinen Antti E. J., and Sharygina Natasha, DAC 2021 - 58th Design Automation Conference