Symbolic execution of object oriented programs with axiomatic summaries
US8046746B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | Aug 4, 2005 |
| Grant date | Oct 25, 2011 |
| Priority date | — |
| Expiry date | Jul 8, 2028 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F11/3688
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
Symbolic execution identifies possible execution paths of a computer program or method, each having certain constraints over the input values. The symbolic execution also records updates of memory locations, e.g. updates of the fields of symbolic objects in the heap of an object oriented program, involving a description of the previous heap, the updated symbolic object, a field identification, and a newly assigned symbolic value. The symbolic execution can also record calls to summarized methods, involving a description of previous calls, an identification of the summarized methods, and its symbolic arguments. The behavior of summarized methods can be expressed by axioms. Axioms describe the relationship between summarized methods under certain conditions. Axioms can be generated from parameterized unit tests. A parameterized unit test is a method with parameters which executes a sequence of calls to methods of an implementation under test; it asserts constraints over the inputs and outputs of the calls. A software testing program receives a parameterized unit test of an implementation under test, and symbolically executes the parameterized unit test. It can re-use axioms generated…
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.