HSolver
User Manual

Stefan Ratschan and Tomáš Dzetkulič and Zhikun She

June 17, 2013

Contents

1 Introduction
2 Invocation
3 The Input
4 Program Termination
5 Produced Output
6 Graphical Output of State Space Analysis
7 Graphical Output of Abstraction
8 The Algorithm
9 Known Bugs

Bibliography

[1]   S. Ratschan and Z. She. Safety verification of hybrid systems by constraint propagation based abstraction refinement. In M. Morari and L. Thiele, editors, Hybrid Systems: Computation and Control, volume 3414 of LNCS, pages 573–589. Springer, 2005.

[2]   S. Ratschan and Z. She. Constraints for continuous reachability in the verification of hybrid systems. In Proc. 8th Int. Conf. on Artif. Intell. and Symb. Comp., AISC’2006, number 4120 in LNCS, pages 196–210. Springer, 2006.

[3]   S. Ratschan and Z. She. Safety verification of hybrid systems by constraint propagation based abstraction refinement. ACM Transactions in Embedded Computing Systems, 6(1):1–23, 2007. article no. 8.

[4]   A. Tiwari. Approximate reachability for linear systems. In O. Maler and A. Pnueli, editors, Hybrid Systems: Computation and Control (HSCC), volume 2623 of LNCS. Springer, 2003.