Incorporating Proofs in a Categorical Attributed Graph Transformation System for Software Modelling and Verification
Bertrand Boisvert, Louis Féraud, Sergei Soloviev
2013
Abstract
This paper deals with model transformations based on attributed graphs transformation. Our approach is based on the categorical approach called Single Pushout. The principal goal being to strengthen the attribute computation part, we generalize our earlier approach based on the use of typed lambda-terms with inductive types and recursion to represent attributes and computation functions. The generalized approach takes terms in variable context as attributes and partial proofs as computation functions that permit to combine computation with proof development and verification. The intended domains of application are the development of cerified software models and semantics models for interactive proof development and verification.
DownloadPaper Citation
in Harvard Style
Boisvert B., Féraud L. and Soloviev S. (2013). Incorporating Proofs in a Categorical Attributed Graph Transformation System for Software Modelling and Verification . In Proceedings of the 1st International Conference on Model-Driven Engineering and Software Development - Volume 1: MODELSWARD, ISBN 978-989-8565-42-6, pages 62-74. DOI: 10.5220/0004321200620074
in Bibtex Style
@conference{modelsward13,
author={Bertrand Boisvert and Louis Féraud and Sergei Soloviev},
title={Incorporating Proofs in a Categorical Attributed Graph Transformation System for Software Modelling and Verification},
booktitle={Proceedings of the 1st International Conference on Model-Driven Engineering and Software Development - Volume 1: MODELSWARD,},
year={2013},
pages={62-74},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0004321200620074},
isbn={978-989-8565-42-6},
}
in EndNote Style
TY - CONF
JO - Proceedings of the 1st International Conference on Model-Driven Engineering and Software Development - Volume 1: MODELSWARD,
TI - Incorporating Proofs in a Categorical Attributed Graph Transformation System for Software Modelling and Verification
SN - 978-989-8565-42-6
AU - Boisvert B.
AU - Féraud L.
AU - Soloviev S.
PY - 2013
SP - 62
EP - 74
DO - 10.5220/0004321200620074