Verics is getting an overhaul and so is this web page, which refers now to both the latest stable version and the new, experimental one, not yet ready for the end user.

Note to the developers: a binary snapshot can be found at and a system-wide PATH setting should already point to the binary executable veric. Examples can be found in the examples/ subdirectory.

Verics is a verification environment running a set of integrated model checkers. It is developed at the Institute of Computer Science, Polish Academy of Sciences. It uses our state-of-the-art methods of bounded and parametric model checking. One of the ideas behind Verics is that a model representation should be friendly to both computer scientists and software developers.

We are currently preparing a new version which will feature updated and new model-checking methods and a common modelling language. It will also support some external verification software like MCMAS, Prism, OSATE or UPPAAL.