Show simple item record

dc.creatorYang, Zijiang
dc.date.accessioned 2007-08-21T00:03:01Z
dc.date.available 2007-08-21T00:03:01Z
dc.date.issued 2000
dc.identifier.urihttp://hdl.handle.net/1911/17391
dc.description.abstract Simulation used to be the most common technique to test the correctness of a system. However, the complexity and size of digital systems has increased drastically during the last few years, which exposes increasingly intractable problems faced by simulation. In order to solve the problems, formal verification was introduced to provide a different approach to validate a system. Model checking has been proposed to make the verification procedure fully automatic. However, the state explosion problem restricts the application of model checking to small systems. Of the different techniques to solve this state explosion problem, one that provided a major breakthrough was that of using techniques to manipulate states symbolically with Binary Decision Diagrams (BDDs). First we use BDDs to represent sets of states that are randomly chosen from a state space. Then we study how the number of states affects the size of BDDs. Based on our research, we provide a formula to calculate the size of BDDs that representing states randomly chosen from a state space. Having a better understanding of BDDs, we are able to compare the main algorithms used in symbolic model checking. (Abstract shortened by UMI.)
dc.format.mimetype application/pdf
dc.language.iso eng
dc.subjectComputer science
dc.title Performance analysis of symbolic reachability algorithms in model checking
dc.type.genre Thesis
dc.type.material Text
thesis.degree.department Computer Science
thesis.degree.discipline Engineering
thesis.degree.grantor Rice University
thesis.degree.level Masters
thesis.degree.name Master of Arts
dc.identifier.citation Yang, Zijiang. "Performance analysis of symbolic reachability algorithms in model checking." (2000) Master’s Thesis, Rice University. http://hdl.handle.net/1911/17391.


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record