Dynamic Dead Variable Analysis

Dynamic dead variable analysis (DDVA) extends traditional static dead variable analysis (SDVA) in the context of model checking through the use of run-time information. The analysis is run multiple times during the course of model checking to create a more precise set of dead variables. The DDVA is evaluated based on the amount of memory used to complete model checking relative to SDVA while considering the extra overhead required to implement DDVA. On several models with a complex control flow graph, DDVA reduces the amount of memory needed by 38-88MB compared to SDVA with a cost of 36 bytes of memory verhead. On several models with loops, DDVA achieved no additional reduction compared to SDVA while requiring no more memory than SDVA.

Name thesis:degree_name

MS

Grantor dc:publisher

Brigham Young University - Provo

Author dc:creator

• Lewis, Micah S.

• static analysis
• model checking
• abstraction
• live variable analysis
• dead variable analysis
• verification
• Computer Sciences

Language dc:language

English

Repository record dc:identifier

https://scholarsarchive.byu.edu/etd/639

OAI identifier oai:identifier

oai:scholarsarchive.byu.edu:etd-1638