Approximating finite domains in symbolic state exploration

• US 20070157180A1
• Filed: 12/30/2005
• Published: 07/05/2007
• Est. Priority Date: 12/30/2005
• Status: Active Grant

• Current Assignee: Zhigu Holdings Limited
• Original Assignee: Microsoft Corporation
• Inventors: Tillmann, Nikolai, Schulte, Wolfram, Grieskamp, Wolfgang
• Granted Patent: US 8,533,680 B2
• Time in Patent Office: Days
• US Class Current: 717/140
• CPC Class Codes: G06F 11/3672 Test management

Abstract

A finite domain approximation for symbolic terms of a symbolic state is derived, given some finite domains for basic terms of the symbolic state. A method is executed recursively for symbolic sub-terms of a symbolic term, providing a domain over-approximation that can then be provided to a solver for determining a more accurate domain. The method can be applied to a wide array of system terms, including, for example, object states, arrays, and runtime types.

Claims

1. A computer-implemented method of determining a finite domain approximation for a symbolic term in a symbolic state representation of a program, wherein the symbolic term comprises a symbolic sub-term, the method comprising:

searching an assumption set for a domain approximation associated with the symbolic term; and

if an associated domain approximation is not found in the assumption set, deriving a domain approximation for the symbolic term according to properties of the symbolic term.

2. The computer-implemented method of claim 1, wherein deriving a domain approximation for the symbolic term comprises deriving a domain approximation for the symbolic sub-term according to properties of the sub-term.

3. The computer-implemented method of claim 1, further comprising assigning an initial domain to the symbolic term.

4. The computer-implemented method of claim 3, wherein the symbolic term is a number variable, and wherein assigning an initial domain comprises calculating a range of the number variable.

5. The computer-implemented method of claim 3, wherein the symbolic term is an object associated with a state, and wherein assigning an initial domain comprises walking over field maps associated with the state.

6. The computer-implemented method of claim 1, further comprising branching to one or more states of an implementation-under-test according to the domain approximation.

7. The computer-implemented method of claim 1, wherein the method executes within a framework at a virtual machine level.

8. The computer-implemented method of claim 1, further comprising applying an additional set of constraints to the domain approximation.

9. The computer-implemented method of claim 1, further comprising calculating an actual domain by supplying the domain approximation to a constraint solver.

10. A computer-readable storage medium containing instructions which can cause a computer to perform a method, the method comprising:

passing a symbolic parameter to a function in a symbolic state representation of a program, the parameter comprising a symbolic sub-parameter;

generating a domain of possible solutions for the symbolic parameter; and

performing a symbolic execution of the function using solutions of the domain to generate a set of actual solutions.

11. The computer-readable storage medium of claim 10, wherein the symbolic parameter comprises an operator.

12. The computer-readable storage medium of claim 10, wherein the symbolic execution of the function using solutions of the domain is performed by a constraint solver.

13. The computer-readable storage medium of claim 12, wherein the constraint solver is a first constraint solver that works in conjunction with a second constraint solver.

14. The computer-readable storage medium of claim 10, wherein the method further comprises simplifying the symbolic parameter.

15. A system for testing programs comprising:

a digital processor; and

a digital memory comprising,

a symbolic term comprising one or more symbolic sub-terms,

a domain derivation unit for determining an approximate set of values for the symbolic term, wherein determining an approximate set of values comprises,

examining an assumption set for a set of values associated with the symbolic term, and

if an associated set of values is not found in the assumption set, deriving a possible set of values of the symbolic term according to properties of the symbolic term.

16. The system of claim 15, further comprising:

a test program; and

a solver, wherein the test program uses the solver to determine an actual set of values for the symbolic term based on the approximate set of values.

17. The system of claim 16, wherein the test program is configured to branch to one or more states in an implementation-under-test according to the actual set of values or the approximate set of values.

18. The system of claim 16, wherein the solver is a first solver working with a second solver.

19. The system of claim 15, wherein determining an approximate set of values further comprises simplifying the symbolic term with a simplifier.

20. The system of claim 15, wherein determining an approximate set of values further comprises assigning an initial set of values to the symbolic term.