• Login
    View Item 
    •   etd@IISc
    • Division of Electrical, Electronics, and Computer Science (EECS)
    • Computer Science and Automation (CSA)
    • View Item
    •   etd@IISc
    • Division of Electrical, Electronics, and Computer Science (EECS)
    • Computer Science and Automation (CSA)
    • View Item
    JavaScript is disabled for your browser. Some features of this site may not work without it.

    Checking Observational Purity of Procedures

    View/Open
    Thesis full text (432.1Kb)
    Author
    Arora, Himanshu
    Metadata
    Show full item record
    Abstract
    We provide two static analysis approaches(using theorem proving) that check if a given (recursive) procedure behaves as if it were stateless, even when it maintains state in global variables. In other words, we check if the given procedure behaves like a mathematical function. In order to eliminate the need for manual annotations, we make use of an invariant that makes use of uninterpreted function symbols. This invariant captures the set of reachable global states in all runs of the procedure, if the procedure is observationally pure. If the procedure is not observationally pure, this invariant has no semantics. Allowing function symbols makes it easier to generate the invariant automatically. The two static analysis are an existential checker and an impurity witness checker. The impurity witness checker outputs a formula whose unsatis fiability implies that the procedure is observationally pure. Whereas, the existential checker outputs a formula that constrains the de finition of the function that the given procedure may implement. Satisfi ability of the formula generated by the existential checker implies that the given procedure is observationally pure. The impurity witness approach works better (empirically) with SMT solvers, whereas the existential approach is more precise on paper. We illustrate our work on examples such as matrix chain multiplication. Examples such as these are not addressable by related techniques in the literature. The closest work to our is by Barnett et al.; this work cannot handle procedures with self recursion. We prove both our approaches to be sound. We have implemented the two static analyses using the Boogie framework and the Z3 SMT solver, and have evaluated our implementation on a number of examples
    URI
    https://etd.iisc.ac.in/handle/2005/5298
    Collections
    • Computer Science and Automation (CSA) [394]

    etd@IISc is a joint service of SERC & J R D Tata Memorial (JRDTML) Library || Powered by DSpace software || DuraSpace
    Contact Us | Send Feedback | Thesis Templates
    Theme by 
    Atmire NV
     

     

    Browse

    All of etd@IIScCommunities & CollectionsTitlesAuthorsAdvisorsSubjectsBy Thesis Submission DateThis CollectionTitlesAuthorsAdvisorsSubjectsBy Thesis Submission Date

    My Account

    LoginRegister

    etd@IISc is a joint service of SERC & J R D Tata Memorial (JRDTML) Library || Powered by DSpace software || DuraSpace
    Contact Us | Send Feedback | Thesis Templates
    Theme by 
    Atmire NV