Zvonimir Rakamaric

Software

• STORM
• smack-0.11.tar.gz
• HAVOC
• straclos decision procedure has been integrated into an available SMT solver MathSAT (big thanks to Roberto Bruttomesso and Alessandro Cimatti for helping out!). The new version of MathSAT extended with straclos (i.e. the theory of unbounded reachability) can be downloaded from the MathSAT homepage.
• straclos 1.0 (Simple TRAnsitive CLOSure logic decision procedure) is available for download. We have been successfully using the decision procedure for predicate abstraction of heap-manipulating programs. You can download the source or Linux binary distribution, and try it out:
  • straclos-1.0.tar.gz
  • straclos-1.0-binary.tar.gz
  Any feedback will be appreciated!