Home | Legals | Data Protection | Sitemap | KIT

Inferring Specifications to Detect Errors in Code

Inferring Specifications to Detect Errors in Code
Author:

Mana Taghdiri, Daniel Jackson

links:
Place:

 Journal of Automated Software Engineering (JASE)– Special issue on selected papers, Volume 14, Issue 1, 2007. (A preliminary version published in ASE’04.)

Date: March 2007

A new technique is presented to statically check a given procedure against a user-provided property. The method requires no annotations; it automatically infers a context-dependent specification for each procedure call, so that only as much information about a procedure is used as is needed to analyze its caller. Specifications are inferred iteratively. Empty specifications are initially used to over-approximate the effects of all procedure calls; these are later refined in response to spurious counterexamples. When the analysis terminates, any remaining counterexample is guaranteed to be valid. However, since the heap is finitized, the absence of a counterexample does not guarantee the validity of the given property.

BibTex

@Article{taghdiri-jackson-2007,
    author  = "M. Taghdiri and D. Jackson",
    title   = {Inferring Specifications to Detect Errors in Code},
    journal = {Journal of Automated Software Engineering (JASE)},
    volume  = {14},
    number  = {1},
    pages   = {87-121},
    year    = {2007}   
}