Symbolic Execution of High-Level Transformations

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.
Tue 1 Nov Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
13:30 - 15:10: Language ValidationSLE at Zürich 2 Chair(s): Ralf LaemmelUniversity of Koblenz-Landau, Germany | |||
13:30 - 13:55 Talk | Automated Testing Support for Reactive Domain-Specific Modelling Languages SLE Bart MeyersUniversity of Antwerp, Belgium, Joachim DenilUniversity of Antwerp, Belgium, István DávidUniversity of Antwerp, Belgium, Hans VangheluweUniversity of Antwerp, Canada DOI | ||
13:55 - 14:20 Talk | Side Effects Take the Blame SLE Felipe Bañados SchwerterUniversity of British Columbia, Canada DOI | ||
14:20 - 14:45 Talk | Symbolic Execution of High-Level Transformations SLE Ahmad Salim Al-SibahiIT University of Copenhagen, Denmark, Aleksandar S. DimovskiIT University of Copenhagen, Denmark, Andrzej WąsowskiIT University of Copenhagen, Denmark Link to publication DOI Pre-print Media Attached | ||
14:45 - 15:00 Talk | Raincode Assembler Compiler (Tool Demo) SLE Volodymyr BlagodarovRaincode, Belgium, Yves JaradinRaincode, Belgium, Vadim ZaytsevRaincode, Belgium DOI |