OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Provably correct graph transformations with small-tALC

Baklanova, Nadezhda and Brenas, Jon Haël and Echahed, Rachid and Percebois, Christian and Strecker, Martin and Tran, Hanh Nhi Provably correct graph transformations with small-tALC. (2015) In: 11th International Conference on ICT in Education, Research, and Industrial Applications (ICTERI 2015), 14 May 2015 - 16 May 2015 (Lviv, Ukraine).

[img]
Preview
(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
240kB

Official URL: http://ceur-ws.org/Vol-1356/paper_14.pdf

Abstract

We present a prototype for executing and verifying graph transformations. The transformations are written in a simple imperative programming language, and pre-and post-conditions as well as loop invariants are specified in the Description Logic ALC (whence the name of the tool). The programming language has a precisely defined operational semantics and a sound Hoare-style calculus. The tool consists of the following sub-components: a compiler to Java for executing the transformations; a verification condition generator; and a tableau prover for an extension of ALC capable of deciding the generated verification conditions. A description of these components and their interaction is the main purpose of this paper.

Item Type:Conference or Workshop Item (Paper)
Additional Information:Thanks to CEUR-WS editor, a free open-access publication service of Sun SITE Central Europe operated under the umbrella of RWTH Aachen University. The definitive version is available at http://ceur-ws.org/ This paper appears in vol 1356 Ceur Workshop Proceedings, ICTERI 2015 : Proceedings of the 11th International Conference on ICT in Education, Research and Industrial Applications: Integration, Harmonization and Knowledge Transfer ISSN : 1613-0073 The definitive version is available at: http://ceur-ws.org/Vol-1356/paper_14.pdf
HAL Id:hal-01517373
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Institut National Polytechnique de Toulouse - INPT (FRANCE)
Other partners > Université Grenoble Alpes - UGA (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UPS (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Laboratory name:
Statistics:download
Deposited By: IRIT IRIT
Deposited On:18 Apr 2017 12:39

Repository Staff Only: item control page