Inferring specifications to detect errors in code |
| |
Authors: | Mana Taghdiri Daniel Jackson |
| |
Affiliation: | (1) Computer Science and AI Lab, Massachusetts Institute of Technology, Cambridge, MA 02139, USA |
| |
Abstract: | 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 in general.
|
| |
Keywords: | Specification inference Modular abstraction Counterexample-guided abstraction refinement Bounded program verification Alloy SAT |
本文献已被 SpringerLink 等数据库收录! |