Home
    • Login
    View Item 
    •   TDL DSpace Home
    • Federated Electronic Theses and Dissertations
    • University of Texas at Austin
    • View Item
    •   TDL DSpace Home
    • Federated Electronic Theses and Dissertations
    • University of Texas at Austin
    • View Item
    JavaScript is disabled for your browser. Some features of this site may not work without it.

    Program analysis with boolean logic solvers

    Thumbnail
    Date
    2007-12
    Author
    Zaraket, Fadi A., 1974-
    Metadata
    Show full item record
    Abstract
    Modern computation systems are very complex. As a result they are very challenging to reason about and validate. Validation techniques based on dynamic analysis—testing— are time consuming and offer no guarantees of correctness. Researchers have proposed static verification techniques which require no testing and are complete. Existing static verification techniques that are based on satisfiability of Boolean formulas in conjunctive normal form validate designs by forcing bounds on the range of variables of a design. Their primary drawback is that they are limited to designs of relatively low complexity. They translate a design expressed in an imperative or a declarative high-level description language to a Boolean formula. There are three limiting aspects of translating high-level designs to conjunctive normal form. (1.) A small increase in the bound on variable ranges can cause a large increase in the size of the translated formula. For example, for an undirected seven-node tree the translation produced one million variables and five million clauses. (2.) Boolean satisfiability solvers are restricted to using optimizations that apply at the level of conjunctive normal form formulas. Finally, (3.) the Boolean formulas often need to be regenerated with higher bounds to ensure the correctness of the translation. This dissertation proposes the use of sequential circuits, Boolean formulas with memory elements and hierarchical structures, and sequential circuit solvers to validate highlevel designs. (1.) Sequential circuits are much more succinct than the pure combinational conjunctive normal form formulas and preserve the high-level structure of the design. (2.) Encoding the problem as a sequential circuit enables the use of a number of powerful automated analysis techniques that have no counterparts for conjunctive normal form formulas. This dissertation applies sequential analysis to both declarative and imperative designs. The results show that it can validate designs with bounds that are orders of magnitude larger than those achievable by the state of the art techniques based on conjunctive normal form analysis.
    URI
    http://hdl.handle.net/2152/3672
    Collections
    • University of Texas at Austin

    DSpace software copyright © 2002-2016  DuraSpace
    Contact Us | Send Feedback
    TDL
    Theme by @mire NV
     

     

    Browse

    All of DSpaceCommunities & CollectionsBy Issue DateAuthorsTitlesSubjectsThis CollectionBy Issue DateAuthorsTitlesSubjects

    My Account

    Login

    DSpace software copyright © 2002-2016  DuraSpace
    Contact Us | Send Feedback
    TDL
    Theme by @mire NV