SMTS

SMTS is a framework for organising and visualizing executions of SMT and PDR in distributed computing environments.  The design is based on a general parallelization technique that supports recursively combining algorithm portfolios and divide-and-conquer with the exchange of learned information.  In addition it allows the user to visually inspect both the parallel execution and the instance structure, and supports interactive, high-level guidance of the algorithm through a web interface.

A virtual image with compiled binaries is available at http://195.176.181.10:8081

A PDF accompanying the virtual image and describing SMTS architecture is available at http://verify.inf.usi.ch/sites/default/files/smts_artifact.pdf

 

Instructions on how to compile smts are available from http://verify.inf.usi.ch/P3.  To run the system, type
 
  ./smts.py -g -o2 -d prova
 
A live GUI demo is available at http://www.inf.usi.ch/phd/marescotti/smt-viewer/.  For security reasons the instance uploading is disabled on the live demo.
 
A visualisation of an SMT instance