Please use this identifier to cite or link to this item: https://doi.org/10.1109/TASE.2012.40
Title: From verification to specification inference
Authors: Chin, W.-N. 
David, C.
Keywords: separation logic
specification inference
structured specifications
verification
Issue Date: 2012
Source: Chin, W.-N.,David, C. (2012). From verification to specification inference. Proceedings - IEEE 6th International Symposium on Theoretical Aspects of Software Engineering, TASE 2012 : 5-6. ScholarBank@NUS Repository. https://doi.org/10.1109/TASE.2012.40
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 to achieve better expressivity (the specification should capture more accurately and concisely the functionality of the corresponding code) and better verifiability (the verification process should succeed in more scenarios than the corresponding verification without the specification enhancements, with better or similar performance). Moreover, we are also interested in providing the necessary tools to assist the user with the important but tedious task of constructing desired specifications. Existing approaches to specification construction tend to be either fully manual or fully automatic. We propose a new framework for specification construction that can be done selectively and incrementally. This framework allows preconditions and post conditions to be selectively inferred via a set of specified variables, that included synthesis for unknown functions and relations. © 2012 IEEE.
Source Title: Proceedings - IEEE 6th International Symposium on Theoretical Aspects of Software Engineering, TASE 2012
URI: http://scholarbank.nus.edu.sg/handle/10635/39895
ISBN: 9780769547510
DOI: 10.1109/TASE.2012.40
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

Page view(s)

38
checked on Dec 9, 2017

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.