Show simple item record

dc.contributor.authorFlanagan, Cormac
dc.date.accessioned 2017-08-02T22:03:33Z
dc.date.available 2017-08-02T22:03:33Z
dc.date.issued 1997-08-28
dc.identifier.urihttps://hdl.handle.net/1911/96471
dc.descriptionThis work was also published as a Rice University thesis/dissertation: http://hdl.handle.net/1911/20475
dc.description.abstract Sophisticated software systems are inherently complex. Understanding, debugging and maintaining such systems requires inferring high-level characteristics of the system's behavior from a myriad of low-level details. For large systems, this quickly becomes an extremely difficult task. MrSpidey is a static debugger that augments the programmers ability to deal with such complex systems. It statically analyzes the program and uses the results of the analysis to identify and highlight any program operation may cause a run-time fault. The programmer can then investigate each potential fault site and, using the graphical explanation facilities of MrSpidey, determine if the fault will really happen or whether the corresponding correctness proof is beyond the analysis's capabilities. In practice, MrSpidey has proven to be an effective tool for debugging program under development and understanding existing programs. The key technology underlying MrSpidey is componential set-based analysis. This is a constraint-based, whole-program analysis for object-oriented and functional programs. The analysis first processes each program component (e.g., module or package) independently, generating and simplifying a constraint system describing the data flow behavior of that component. The analysis then combines and solves these simplified constraint systems to yield invariants characterizing the run-time behavior of the entire program. This component-wise approach yields an analysis that handles significantly larger programs than previous analyses of comparable accuracy. The simplification of constraint systems raises a number of questions. In particular, we need to ensure that simplification preserves the observable behavior, or solution space, of a constraint system. This dissertation provides a complete proof-theoretic and algorithmic characterization of the observable behavior of constraint systems, and establishes a close connection between the observable equivalence of constraint systems and the equivalence of regular tree grammars. We exploit this connection to develop a complete algorithm for deciding the observable equivalence of constraint systems, and to adapt a variety of algorithms for simplifying regular tree grammars to the problem of simplifying constraint systems. The resulting constraint simplification algorithms yield an order of magnitude reduction in the size of constraint systems for typical program expressions.
dc.format.extent 173 pp
dc.language.iso eng
dc.rights You are granted permission for the noncommercial reproduction, distribution, display, and performance of this technical report in any format, but this permission is only for a period of forty-five (45) days from the most recent time that you verified that this technical report is still available from the Computer Science Department of Rice University under terms that include this permission. All other rights are reserved by the author(s).
dc.title Effective Static Debugging via Componential Set-Based Analysis
dc.type Technical report
dc.date.note August 28, 1997
dc.identifier.digital TR97-287
dc.type.dcmi Text
dc.identifier.citation Flanagan, Cormac. "Effective Static Debugging via Componential Set-Based Analysis." (1997) https://hdl.handle.net/1911/96471.


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record