On-the-Fly Dynamic Dead Variable Analysis

State explosion in model checking continues to be the primary obstacle to widespread use of software model checking. The large input ranges of variables used in software is the main cause of state explosion. As software grows in size and complexity the problem only becomes worse. As such, model checking research into data abstraction as a way of mitigating state explosion has become more and more important. Data abstractions aim to reduce the effect of large input ranges. This work focuses on a static program analysis technique called dead variable analysis. The goal of dead variable analysis is to discover variable assignments that are not used. When applied to model checking, this allows us to ignore the entire input range of dead variables and thus reduce the size of the explored state space. Prior research into dead variable analysis for model checking does not make full use of dynamic run-time information that is present during model checking. We present an algorithm for intraprocedural dead variable analysis that uses dynamic run-time information to find more dead variables on-the-fly and further reduce the size of the explored state space. We introduce a definition for the maximal state space reduction possible through an on-the-fly dead variable analysis and then show that our algorithm produces a maximal reduction in the absence of non-determinism.

Name thesis:degree_name

MS

Grantor dc:publisher

Brigham Young University - Provo

Author dc:creator

• Self, Joel P.

• model checking
• computer science
• static
• static analysis
• dynamic analysis
• analysis
• program
• program analysis
• Estes
• GDB
• dead variable analysis
• dead variable
• live variable
• live variable analysis
• CFG
• abstraction
• data abstraction
• on-the-fly
• static program analysis
• control flow graph
• software model checking
• state space
• depth first search
• state explosion
• state explosion problem
• Computer Sciences

Language dc:language

English

Repository record dc:identifier

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

OAI identifier oai:identifier

oai:scholarsarchive.byu.edu:etd-1885