Symbolic Model Checking of Software

摘要: Abstract Model checking is a popular formal verification technique for both software and hardware. The of concurrent predominantly employs explicit-state model checkers, such as SPIN, that use partial-order reduction main to deal with large state spaces efficiently. In the hardware domain, introduction symbolic has been considered breakthrough, allowing systems clearly out-of-reach any checker. This paper introduces I m P roviso , new algorithm efficiently combines advantages exploration. M ROVISO uses implicit BDD representations space transition relation together in-stack proviso efficient reduction. approach inspired by T wophase checking. Initial experimental results show proposed improves existing can be used tackle problems are not tractable using methods.