An Introduction to the Verification of Hybrid Systems Using Ariadne

We introduce the verification of hybrid systems as offered by the open-source framework called ariadne. The ariadne c++ library exploits approximation techniques based on the theory of computable analysis for implementing formal verification algorithms based on reachability analysis. We demonstrate the tool using a classical example of a controlled water tank system.keywordsariadnewater tank examplehybrid automatareachable setlower semanticsthese keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves