Title: An introduction to the model verifier 'verds'

Speaker: Wenhui Zhang

Time: 3.00pm, Wednesday September 15

Venue: Lecture room, Lab for Computer Science, 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.