PV4 MCHyperproves given properties on a given circuit

Hardware model checker for hyperproperties

Application domain/field

Type of tool

Model checker

Expected input


Expected output

It will either report that the property is proven, or it will provide a counterexample. You can also inspect the generated circuit. The user can also choose to get more verbose output.


MCHyper is a model checker for synchronous HyperLTL properties. It can handle up to one quantifier alternation. HyperLTL allows the user to specify temporal properties that relate multiple computation traces, also called hyperproperties. Therefore, the user can check a.o. information-flow properties and noninterference between two traces. It uses ABC as the backend for checking the reachability of a violation. If given a Verilog system as input, it will be converted into an Aiger circuit using Yosys.
Hardware HyperLTL Model checking


Related papers

Verifying Hyperliveness

Last publication date

12 July 2019

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.