up: Publications |
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.
Online Copy |
BibTeX Entry |
@inproceedings{makhlouf16:_combin_dynam_static_analy_help, author = {Amani Makhlouf and Hanh Nhi Tran and Christian Percebois and Martin Strecker}, title = {Combining Dynamic and Static Analysis to Help Develop Correct Graph Transformations}, booktitle = {Tests and Proofs - 10th International Conference, {TAP} 2016, Held as Part of {STAF} 2016, Vienna, Austria, July 5-7, 2016, Proceedings}, editor = {Bernhard K. Aichernig and Carlo A. Furia}, series = {Lecture Notes in Computer Science}, volume = {9762}, publisher = {Springer}, pages = {183--190}, year = 2016, url = {http://dx.doi.org/10.1007/978-3-319-41135-4_11}, doi = {10.1007/978-3-319-41135-4_11}, }
Tue Oct 25 11:49:22 CEST 2016 |