Specification, Verification and Inference (Invited Talk)

Author Wei-Ngan Chin



PDF
Thumbnail PDF

File

OASIcs.FSFMA.2013.2.pdf
  • Filesize: 202 kB
  • 1 pages

Document Identifiers

Author Details

Wei-Ngan Chin

Cite AsGet BibTex

Wei-Ngan Chin. Specification, Verification and Inference (Invited Talk). In 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013). Open Access Series in Informatics (OASIcs), Volume 31, p. 2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
https://doi.org/10.4230/OASIcs.FSFMA.2013.2

Abstract

Traditionally, the focus of specification mechanism has been on improving its ability to cover a wider range of problems more accurately, while the effectiveness of verification is left to the underlying theorem provers. Our work attempts a novel approach, where the focus is on designing good specification mechanisms that can achieve both better expressiveness and better verifiability. Moreover, we shall also highlight a unified specification mechanism that can be used for both verification and inference. Our framework allows preconditions and postconditions to be selectively inferred via a set of uninterpreted relations which are computed using bi-abduction, and modularly synthesized to support concise specification for program codes.
Keywords
  • Expressive Specification
  • Automated Verification
  • Specification Inference

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail