RED
Region-Encoding Diagram
Technology for Fully Symbolic Verification of Timed/Hybrid Software Systems
by Farn Wang
Dept. of Electrical Engineering, National Taiwan University
Taipei, Taiwan 106, ROC
TEL:‰n2-33663602
FAX:‰n2-23671909

Important Note:

Please read the license carefully. Fill in all the fields in the form. Fields with an asterisk in front are mandatory, while others are optional. If possible, please fill in all the fields and then click the "Send License Form and download" button. No information provided will be used by any other person besides the authors themselves for the sole purpose of tool registration and future update notification. Thank you very much!

RED
Region-Encoding Diagram
LICENSE AGREEMENT

The tool, "Region-Encoding Diagram" (RED), is provided as is. Any type of damage or loss resulting from either a direct or an indirect application of the tool is NOT the responsibility of the authors. The users of the tool must be solely responsible for all side-effects, losses, damages, and consequences resulting through the use of the tool.

The tool must be used only for educational and research purposes. This license only covers the afore-mentioned two purposes. For all other purposes including commercial use of the tool, the users must obtain another license prior to any such usage. The authors may be contacted directly for other license agreements.

Users of the tool may request for technical help from the authors, but no definite technical help of any sort is guaranteed. All help is provided only at the discretion of the authors.

Agree?		Yes No
Purpose: (multiple choices allowed)		[1] Formal Verification Research [2] Verification Experiments [3] Teaching or Education [4] Just curious
Tools Used: (multiple choices allowed)		None UPPAAL Kronos HyTech red SMV Others
*Name:
*Affiliation:		Organization: None University Research Institute Industry Others
*Position:
*E-Mail Address:
Telephone Number:
Mailing Address:
Comments:
		Receive notice on future tool updates?

 

RED version 5.5 with HRD (Hybrid-Restriction Diagram) + Clock-Restriction Diagram (CRD) technology
for the verification of timed systems and linear hybrid systems
Please choose a version for your platform to download!
version 5.5 on Linux
¡@

AMAST 2004 paper for event and fairness assumptions.

CAV 2004 paper for HRD technology (A preliminary version is also in ACM CoRR, user:cs.DS/0306113).

¡@

---