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).
|
(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 - Toulouse INP (FRANCE) Other partners > Université Grenoble Alpes - UGA (FRANCE) Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (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 On: | 18 Apr 2017 12:39 |
Repository Staff Only: item control page
