@inbook {IOPORT.06105574,
    author       = {Sulzmann, Martin and Zechner, Axel},
    title        = {Model checking DSL-generated C source code.},
    year         = {2012},
    booktitle    = {Model checking software. 19th international workshop, SPIN 2012, Oxford, UK, July 23--24, 2012. Proceedings},
    isbn         = {978-3-642-31758-3},
    pages        = {241-247},
    publisher    = {Berlin: Springer},
    doi          = {10.1007/978-3-642-31759-0_18},
    abstract     = {Summary: We report on the application of SPIN for model-checking C source code which is generated out of a textual domain-specific language (DSL). We have built a tool which automatically generates the necessary SPIN wrapper code using (meta-)information available at the DSL level. The approach is part of a larger tool-chain for developing mission critical applications. The main purpose of SPIN is for bug-finding where error traces resulting from SPIN can be automatically replayed at the DSL level and yield concise explanations in terms of a temporal specification DSL. The tool-chain is applied in some large scale industrial applications.},
    identifier   = {06105574},
}