Title:An introduction to the model verifier 'verds'
Speaker: Wenhui Zhang
Venue:Lecture Room, Level 3 Building #5, Institute of Software, CAS
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.