Pitu, M. and Grijincu, D. and Li, P. and Saleem, A. and Monahan, Rosemary and O'Donoghue, Diarmuid (2013) Arís: Analogical Reasoning for reuse of Implementation & Specification. Proceedings of AI4FM 2013.

Download (119kB)

Abstract

Formal methods and formal verification of source code has been used extensively in the past few years to create dependable software systems. However, although formal languages like Spec# or JML are quite popular, the set of verified implementations remains small. Our work aims to automate some of the steps involved in writing specifications and their implementations, by reusing existing verified programs i.e. for a given implementation, we aim to retrieve similar verified code and then reapply the missing specification that accompanies that code. Similarly, for a given specification, we aim to retrieve code with a similar specification and use its implementation to generate the missing implementation.

Item Type:	Article
Keywords:	Arís; Analogical Reasoning; Implementation & Specification;
Academic Unit:	Faculty of Science and Engineering > Computer Science
Item ID:	4497
Depositing User:	Dr. Diarmuid O'Donoghue
Date Deposited:	16 Sep 2013 15:27
Journal or Publication Title:	Proceedings of AI4FM 2013
Publisher:	Department of Computer Science, Heriot-Watt University
Refereed:	Yes
URI:	Publisher
Use Licence:	This item is available under a Creative Commons Attribution Non Commercial Share Alike Licence (CC BY-NC-SA). Details of this licence are available here

Repository Staff Only(login required)

Item control page

Downloads

Origin of downloads