Please use this identifier to cite or link to this item:
https://doi.org/10.1007/s10009-014-0306-5
DC Field | Value | |
---|---|---|
dc.title | Expressive program verification via structured specifications | |
dc.contributor.author | Gherghina, C. | |
dc.contributor.author | David, C. | |
dc.contributor.author | Qin, S. | |
dc.contributor.author | Chin, W.-N. | |
dc.date.accessioned | 2016-05-17T10:45:11Z | |
dc.date.available | 2016-05-17T10:45:11Z | |
dc.date.issued | 2014-03-28 | |
dc.identifier.citation | Gherghina, C., David, C., Qin, S., Chin, W.-N. (2014-03-28). Expressive program verification via structured specifications. International Journal on Software Tools for Technology Transfer. ScholarBank@NUS Repository. https://doi.org/10.1007/s10009-014-0306-5 | |
dc.identifier.issn | 14332779 | |
dc.identifier.uri | http://scholarbank.nus.edu.sg/handle/10635/123998 | |
dc.description.abstract | Conventional specifications typically have a flat structure that is based primarily on the underlying logic. Such specifications lack structures that could provide better guidance to the verification process. In this work, we propose to add three new structures to a specification framework for separation logic to achieve a more precise and better guided verification for pointer-based programs. The newly introduced structures empower users with more control over the verification process in the following ways: (1) case analysis can be invoked to take advantage of disjointedness conditions in the logic, (2) early, as opposed to late, instantiation can minimise the use of existential quantification and (3) novel formulae structuring can provide better reuse of the verification process. Initial experiments have shown that structured specifications can lead to more precise verification without incurring any performance overhead. To support our proposal, we shall illustrate the usage of structured specifications in the context of proving termination and we will briefly outline the impact of our proposal on a recent development focussed on verifying the FreeRTOS scheduler Ferreira et al. (Int. J. Softw. Tools Technol. Trans. 2014). © 2014 Springer-Verlag Berlin Heidelberg. | |
dc.description.uri | http://libproxy1.nus.edu.sg/login?url=http://dx.doi.org/10.1007/s10009-014-0306-5 | |
dc.source | Scopus | |
dc.subject | Case analysis | |
dc.subject | Separation logic | |
dc.subject | Structured specifications | |
dc.type | Article | |
dc.contributor.department | COMPUTER SCIENCE | |
dc.description.doi | 10.1007/s10009-014-0306-5 | |
dc.description.sourcetitle | International Journal on Software Tools for Technology Transfer | |
dc.identifier.isiut | 000209673200003 | |
Appears in Collections: | Staff Publications |
Show simple item record
Files in This Item:
There are no files associated with this item.
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.