Browsing by Subject "Constraint solving"
Now showing 1 - 3 of 3
Results Per Page
Sort Options
Item Enhancing symbolic execution using memoization and incremental techniques(2013-08) Yang, Guowei, active 2013; Khurshid, SarfrazThe last few years have seen a resurgence of interest in the use of symbolic execution--program analysis technique developed more than three decades ago to analyze program execution paths. However, symbolic execution remains an expensive technique and scaling it remains a key technical challenge. There are two key factors that contribute to its cost: (1) the number of paths that need to be explored and (2) the cost of constraint solving, which is typically required for each path explored. Our insight is that the cost of symbolic execution can be reduced by an incremental approach, which uses static analysis and dynamic analysis to focus on relevant parts of code and reuse previous analysis results, thereby addressing both the key cost factors of symbolic execution. This dissertation presents Memoized Incremental Symbolic Execution, a novel approach that embodies our insight. Using symbolic execution in practice often requires several successive runs of the technique on largely similar underlying problems where successive problems differ due to some change, which may be to code, e.g., to fix a bug, to analysis parameters, e.g., to increase the path exploration depth, or to correctness properties, e.g., to check against stronger specifications that are written as assertions in code. Memoized Incremental Symbolic Execution, a three-fold approach, leverages the similarities in the successive problems to reduce the total cost of applying the technique. Our prototype tool-set is based on the Symbolic PathFinder. Experimental results show that Memoized Incremental Symbolic Execution enhances the efficacy of symbolic execution.Item Improving constraint-based test input generation using Korat(2015-05) Srinivasan, Raghavendra; Khurshid, SarfrazKorat is an existing technique for test input generation using imperative constraints that describe properties of desired inputs written as Java predicates, termed RepOk methods, which are executable checks for those properties. Korat efficiently prunes the space of candidate inputs for the RepOk method by executing it on candidate inputs and monitoring the object fields that RepOk accesses in deciding if the properties are satisfied. While Korat generates inputs effectively, its correctness and efficiency rely on two assumptions about the RepOk methods. For correctness, Korat assumes the RepOk methods do not use the Java reflection API for field accesses; the use of reflection renders Korat unable to enumerate all desired inputs. For efficiency, Korat assumes the RepOk methods do not make unnecessary field accesses, which can reduce the effectiveness of Korat’s pruning. Our thesis addresses both these limitations. To support reflection, we build on the core Korat to enhance it such that it can monitor field accesses based on reflection. To assist the users with writing RepOk’s, we introduce a static analysis tool that detects potential places where the input RepOk may be edited to enhance performance of Korat. We also present experimental results using a suite of standard data structure subjects.Item Milao : a novel framework for mixed imperative and declarative formulation and solving of structural constraints(2009-12) Narayanan, Vidya Priyadarshini; Khurshid, Sarfraz; Perry, Dewayne E.Advances in constraint solving and increases in processing power have enabled new approaches for automating specification-based testing. However, writing specifications and scaling techniques that utilize them remain challenging. We introduce Milao -- a novel framework for mixed imperative and declarative formulation and solving of structural constraints -- which addresses both these challenges. One, Milao introduces a mixed style for writing specifications using a combination of declarative and imperative styles, which provides flexibility in specification formulation and reduces its burden on the user. Two, it introduces a mixed technique for solving constraints using a combination of solvers in synergy. As enabling technologies, the Alloy tool-set and the Java PathFinder model checker are used. Initial experiments witness the benefits of our framework.