dReach/dReal

dReach/dReal

Description: dReach is a tool for safety verification of hybrid systems.

It answers questions of the type: Can a hybrid system run into an unsafe region of its state space? This question can be encoded to SMT formulas, and answered by our SMT solver. dReach is able to handle general hyrbid systems with nonlinear differential equations and complex discrete mode-changes.

Since dReal implements a δ-complete decision procedure, dReach performs “bounded δ-complete reachability analysis”.

dReal is an automated reasoning tool. It focuses on solving problems that can be encoded as first-order logic formulas over the real numbers. Its special strength is in handling problems that involve a wide range of nonlinear real functions. dReal implements the framework of δ-complete decision procedures.

VO Integration: No

Active: Yes

Available Benchmarks: Yes

Website: http://dreal.github.io/dReach/

Download: Links to git repository and source can be found here.

Documentation: The website contains example pages for dReach and dReal, along with benchmarks.

Contact: Here is a list of people associated with the tools.

Excerpt and graphic from: http://dreal.github.io/dReach/