Towards Complete Reasoning about Axiomatic Specifications

paper ps   
To support verification of expressive properties of functional programs, we consider algebraic style specifications that may relate multiple user-defined functions, and compare multiple invocations of a function for different arguments. We present decision procedures for reasoning about such universally quantified properties of functional programs, using local theory extension methodology. We establish new classes of universally quantified formulas whose satisfiability can be checked in a complete way by finite quantifier instantiation. These classes include single-invocation axioms that generalize standard function contracts, but also certain many-invocation axioms, specifying that functions satisfy congruence, injectivity, or monotonicity with respect to abstraction functions, as well as conjunctions of some of these properties. These many-invocation axioms can specify correctness of abstract data type implementations as well as certain information-flow properties. We also present a decidability-preserving construction that enables the same function to be specified using different classes of decidable specifications on different partitions of its domain.

Citation

Swen Jacobs and Viktor Kuncak. Towards complete reasoning about axiomatic specifications. In Verification, Model Checking, and Abstract Interpretation (VMCAI), 2011.

BibTex Entry

@inproceedings{JacobsKuncak11TowardsCompleteReasoningaboutAxiomaticSpecifications,
  author = {Swen Jacobs and Viktor Kuncak},
  title = {Towards Complete Reasoning about Axiomatic Specifications},
  booktitle = {Verification, Model Checking, and Abstract Interpretation (VMCAI)},
  year = 2011,
  abstract = { To support verification of expressive properties of
  functional programs, we consider algebraic style
  specifications that may relate multiple user-defined
  functions, and compare multiple invocations of a function
  for different arguments.
  We present decision procedures for reasoning about such universally quantified
  properties of functional programs, using local
  theory extension methodology. We establish new classes of
  universally quantified formulas whose satisfiability can
  be checked in a complete way by finite quantifier
  instantiation. These classes include single-invocation
  axioms that generalize standard function contracts, but
  also certain many-invocation axioms, specifying that
  functions satisfy congruence, injectivity, or monotonicity
  with respect to abstraction functions, as well as conjunctions
  of some of these properties. These many-invocation
  axioms can specify correctness of abstract data type
  implementations as well as certain information-flow
  properties.  We also present a decidability-preserving construction that enables
  the same function to be specified using different classes
  of decidable specifications on different partitions of its
  domain. }
}