Nová verze webových stránek Ústavu informatiky AV ČR v.v.i. je přístupná zde ...


by Stefan Ratschan

RSolver is a program for solving quantified inequality constraints.
Problems like projecting the solution set of a set of inequality constraints to two dimensions, or parametric robust stability of linear differential equations can be directly formulated as such constraints.

Main Paper Describing Method: Stefan Ratschan - Efficient Solving of Quantified Inequality Constraints over the Real Numbers.
ACM Transactions on Computational Logic, Volume 7, Number 4, pp. 723-748, 2006

More information can be found at


by Stefan Ratschan (with Zhikun She, Tomáš Dzetkulič)

HSolver is a program for verification of hybrid systems based on the constraint solver RSOLVER.
Unlike other packages its correctness does not depend on floating point rounding errors. It can handle non-linear ordinary differential equations, but is not optimized for simpler continuous dynamics.

Main Paper Describing Method: Stefan Ratschan and Zhikun She - Safety Verification of Hybrid Systems by Constraint Propagation Based Abstraction Refinement. ACM Transactions in Embedded Computing Systems, Volume 6, Number 1, 2007

Acknowledgements: This software packages was supported by GA ČR grant P202/12/J060, and MŠMT grant OC10048.

More information can be found at


Bang3 is a distributed multi-agent system for building hybrid artificial intelligence models.
For more information visit our homepage or mail to  


GUHA (General Unary Hypothesis Automaton) is one of data mining methods (basicaly a method for exploratory data analysis), which enables the recognition of regularities in empirical data. 

Its aim is to offer "all interesting" hypotheses supported by given data and differs from many statistacally based data mining methods by the emphasis on polyfactorial hypotheses searching. 

In the last 30 years different GUHA versions have been successfully applied in the following areas: medicine, sociology, psychology and reliability studies in the automotive industry. 

Now there is new implementation of the GUHA method for Windows 95/98/NT platform available. This implementation called as GUHA +- project can be downloaded here (to unzip use -d switch). Software is licensed as freeware. Instalation includes reference manual. Another more user friedly manual including description of GUHA +- package installation is here as zipped postscript or hereas zipped MS Word document. For other info mail to 

HTML version of the PC-GUHA Brief manual is also available. PC-GUHA is an old implementation of GUHA method for DOS. It will be also available for download, but now it is under process of recompilation so check this site in future. 


UFO is an interactive system for universal functional optimization that serves for solving both dense medium-size and sparse large-scale optimization problems.

Nová verze webových stránek Ústavu informatiky AV ČR v.v.i. je přístupná zde ...