Abstract:
The model verifier 'verds' and its theoretical foundations
are introduced. There are two distinguished features of 'verds'.
One is that it supports boolean diagram model checking, a kind
of symbolic model checking based on boolean diagrams for boolean
function manipulation.
It differs from the usual symbolic model checking based on
decision diagrams.
Initial experimental evaluation based on random boolean programs
shows that it has significant advantages over symbolic model checking
based on decision diagrams.
The other feature is that it supports bounded semantics model checking,
a kind of bounded model checking based on bounded semantics that
can be used for both bounded verification and bounded error detection.
It differs from the usual bounded model checking based on bounded semantics
of existential temporal logics.
Initial experimental evaluation shows that it has advantages over
symbolic model checking in a large percentage of the test cases,
where both verification and error detection problems are well represented.