Ajankovil, Kuruvilla George and O'Donoghue, Diarmuid and Monahan, Rosemary (2021) Creating new Program Proofs by Combining Abductive and Deductive Reasoning. In: International Conference on Computational Creativity ICCC, September 2021.

Preview

Download (762kB) | Preview

Abstract

We describe recent work on the Aris system that creates and verifies new formal specifications for pre-existing source code. We describe Aris in terms of the abductive reasoning system that suggest possible specifications and then uses an existing deductive verifier to evaluate these creations. This paper focuses on the abduction system that creates new formal specifications by leveraging a small set of inspiring artefacts to augment a subset of candidate problems. This employs knowledge graphs to represent the raw data (i.e., source code), discovering latent similarities between graphs using a graph-matching process. Results are presented for the C# programming language with novel creations and its sister language called Code Contracts. We outline ampliative creativity, whereby newly created artefacts drive subsequent creative episodes beyond the initially perceived limitations. We also outline some recent work towards transferring specifications between the C# and Java programming languages.

Item Type:	Conference or Workshop Item (Paper)
Keywords:	Creating; new Program Proofs; Combining Abductive; Deductive Reasoning;
Academic Unit:	Faculty of Science and Engineering > Computer Science Faculty of Science and Engineering > Research Institutes > Hamilton Institute
Item ID:	15752
Depositing User:	Dr. Diarmuid O'Donoghue
Date Deposited:	29 Mar 2022 15:28
Refereed:	Yes
URI:	Organisation
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