Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Conferences, Workshops, Symposiums, and Seminars
  4. Towards Complete Reasoning about Axiomatic Specifications
 
Loading...
Thumbnail Image
conference paper

Towards Complete Reasoning about Axiomatic Specifications

Jacobs, Swen
•
Kuncak, Viktor  
2011
Verification, Model Checking, And Abstract Interpretation
Verification, Model Checking, and Abstract Interpretation (VMCAI)

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.

  • Details
  • Metrics
Type
conference paper
DOI
10.1007/978-3-642-18275-4_20
Web of Science ID

WOS:000297039800020

Author(s)
Jacobs, Swen
•
Kuncak, Viktor  
Date Issued

2011

Publisher

Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa

Published in
Verification, Model Checking, And Abstract Interpretation
ISBN of the book

978-3-642-18274-7

Series title/Series vol.

Lecture Notes in Computer Science; 6538

Start page

278

End page

293

Subjects

Extensions

Peer reviewed

REVIEWED

Written at

EPFL

EPFL units
LARA  
Event name
Verification, Model Checking, and Abstract Interpretation (VMCAI)
Available on Infoscience
May 25, 2011
Use this identifier to reference this record
https://infoscience.epfl.ch/handle/20.500.14299/67865
Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés