Abstract. We present a new open source model checker, opaal, for automatic verification of models using lattice automata. Lattice automata allow the users to incorporate abstracti...
Abstract. Several verification methods involve reasoning about multi-valued systems, in which an atomic proposition is interpreted at a state as a lattice element, rather than a B...