OASIcs.FSFMA.2013.2.pdf
- Filesize: 202 kB
- 1 pages
Document
Specification, Verification and Inference (Invited Talk)
Author
-
Part of:
Volume:
1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)
Series: Open Access Series in Informatics (OASIcs) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2013-07-14
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
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)
0PDF Downloads