Symbolic execution of high-level transformations
- 20 October 2016
- conference paper
- conference paper
- Published by Association for Computing Machinery (ACM) in Proceedings of the 2016 ACM SIGPLAN International Conference on Software Language Engineering
- p. 207-220
- https://doi.org/10.1145/2997364.2997382
Abstract
Transformations form an important part of developing domain specific languages, where they are used to provide semantics for typing and evaluation. Yet, few solutions exist for verifying transformations written in expressive high-level transformation languages. We take a step towards that goal, by developing a general symbolic execution technique that handles programs written in these high-level transformation languages. We use logical constraints to describe structured symbolic values, including containment, acyclicity, simple unordered collections (sets) and to handle deep type-based querying of syntax hierarchies. We evaluate this symbolic execution technique on a collection of refactoring and model transformation programs, showing that the white-box test generation tool based on symbolic execution obtains better code coverage than a black box test generator for such programs in almost all tested cases.Keywords
Funding Information
- Det Frie Forskningsråd (0602-02327B)
This publication has 9 references indexed in Scilit:
- Symbolic execution of high-level transformationsPublished by Association for Computing Machinery (ACM) ,2016
- Unifying functional and object-oriented programming with ScalaCommunications of the ACM, 2014
- TETRABox - A Generic White-Box Testing Framework for Model TransformationsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2013
- A survey of approaches for verifying model transformationsSoftware and Systems Modeling, 2013
- Efficient and formal generalized symbolic executionAutomated Software Engineering, 2011
- Stratego/XT 0.17. A language and toolset for program transformationScience of Computer Programming, 2008
- Uniform boilerplate and list processingPublished by Association for Computing Machinery (ACM) ,2007
- Verifying metamodel coverage of model transformationsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2006
- The Verifying Compiler, a Grand Challenge for Computing ResearchLecture Notes in Computer Science, 2005