Makhlouf, Amani
and Tran, Hanh Nhi and Percebois, Christian and Strecker, Martin
Combining Dynamic and Static Analysis to Help Develop Correct Graph Transformations.
(2016)
In: International Conference on Tests and Proofs (TAP 2016), 5 July 2016 - 7 July 2016 (Vienna, Austria).
|
(Document in English)
PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader 644kB |
Official URL: https://doi.org/10.1007/978-3-319-41135-4_11
Abstract
Developing provably correct graph transformations is not a trivial task. Besides writing the code, a developer must as well specify the pre- and post-conditions. The objective of our work is to assist developers in producing such a Hoare triple in order to submit it to a formal verification tool. By combining static and dynamic analysis, we aim at providing more useful feedback to developers. Dynamic analysis helps identify inconsistencies between the code and its specifications. Static analysis facilitates extracting the pre- and post-conditions from the code. Based on this proposal, we implemented a prototype that allows running, testing and proving graph transformations written in small-tALC, our own transformation language.
| Item Type: | Conference or Workshop Item (Paper) |
|---|---|
| Additional Information: | Thanks to Springer editor. This papers appears in volume 9762 of Lecture Notes in Computer Science ISSN: 0302-9743 ISBN: 978-3-319-41134-7 The original PDF is available at: https://link.springer.com/chapter/10.1007/978-3-319-41135-4_11 |
| HAL Id: | hal-02559762 |
| Audience (conference): | International conference proceedings |
| Uncontrolled Keywords: | |
| Institution: | Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE) French research institutions > Centre National de la Recherche Scientifique - CNRS (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: | 22 Apr 2020 10:14 |
Repository Staff Only: item control page
