The following software tools are currently available, sorted approximately according to how recently they have been updated:

  • Stainless - Verifier for Scala
  • Leon - Verifier and Synthesizer for Scala
  • CVC4 - CVC4 SMT Solver
  • Orb - Resource Bound Inference for Functional Programs
  • Rosa - Compiler for Reals
  • StringSolver - A solver for string transformations, file renaming and semi-automated bash commands.

We believe many of these systems are already useful, even though their explicit goal was to explore and evaluate research results. If you consider some of them as toys, however, we will be flattered, because we believe that toys are at least as essential for the development of science and technology as they are for the development of children.