We present ABS, a software for Abstraction-Based Synthesis of controllers for continuous-state control systems. The tool distinguishes itself from previously known such software by being formally correct, i.e., any controller synthesized by ABS is mathematically guaranteed to solve the control problem provided as input. ABS achieves this quality by providing an input language with mathematically defined semantics and a respective compiler, and by carefully taking into account all numerical and rounding errors that might be incurred at either compile- or run-time. To mitigate computational overhead caused by the aforementioned approach, ABS implements, e.g. on-the-fly synthesis algorithms with greatly reduced memory requirement. The tool is currently applicable to invariance and reachability problems and requires state measurement. We discuss structure, algorithmic details and basic usage of ABS, and we demonstrate on two examples that its performance compares favorably with that of competing, not formally correct synthesis software. The source code of ABS is publicly available. See http://www.reiszig.de/gunther/pubs/ABS.html