Orange presents Octant – a front-end for Z3 SMT solver

Octant is a fast Datalog implementation that can be used to check compliance properties on an OpenStack cloud. It uses the automatic theorem prover Microsoft Z3 and offers access to the main Neutron and Nova tables (concerning networks, ports, security groups, routers, servers).

The code, which includes the documentation as well, is now available on Orange-Opensource GitHub under Apache 2.0 license.