Symbolic runtime checking of quantified contracts
US8387021B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | Sep 26, 2008 |
| Grant date | Feb 26, 2013 |
| Priority date | — |
| Expiry date | Jul 7, 2031 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F11/3692
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
An extension of symbolic execution for programs involving contracts with quantifiers over large and potentially unbounded domains is described. Symbolic execution is used to generate, from a program, concrete test cases that exhibit mismatches between the program code and its contracts with quantifiers. Quantifiers are instantiated using symbolic values encountered during a set of exhibited runs. In this setting, quantifier instantiation is limited to values supplied to or produced by a symbolic execution. Quantifier instantiation is controlled by performing a matching algorithm that uses run-time values of input and program variables in order to guide and limit the set of quantifier instantiations. With a sufficient set of instances, test cases are derived that directly witness limitations of the auxiliary assertions.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.