This is an old revision of the document!
Software
The following software tools are currently available, sorted approximately according to how recently they have been updated:
- Leon - Verifier and Synthesizer for Scala
- Orb - Resource Bound Inference for Functional Programs
- Rosa - Compiler for Reals
- StringSolver - A solver for string transformations, file renaming and semi-automated bash commands.
- InSynth - Interactive Synthesis
- Pong Designer - Programming Games by Demonstration
- Eldarica - Predicate Abstraction Engine
- SmartFloat - Numerical Error Estimator
- Phantm - PHp ANalyzer for Type Mismatch
- RegSy - Regular Synthesis over Unbounded Domains
- Comfusy - Complete Functional Synthesis
- Nenofar - Negation Normal Form Automated Reasoner
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.
Two links to industrial-strength systems: