@inproceedings{1f83eac78f35458694b5281f39b8781b,
title = "Context generation from formal specifications for C analysis tools",
abstract = "Analysis tools like abstract interpreters, symbolic execution tools and testing tools usually require a proper context to give useful results when analyzing a particular function. Such a context initializes the function parameters and global variables to comply with function requirements. However it may be error-prone to write it by hand: the handwritten context might contain bugs or not match the intended specification. A more robust approach is to specify the context in a dedicated specification language, and hold the analysis tools to support it properly. This may mean to put significant development efforts for enhancing the tools, something that is often not feasible if ever possible. This paper presents a way to systematically generate such a context from a formal specification of a C function. This is applied to a subset of the ACSL specification language in order to generate suitable contexts for the abstract interpretation-based value analysis plug-ins of Frama-C, a framework for analysis of code written in C. The idea here presented has been implemented in a new Frama-C plug-in which is currently in use in an operational industrial setting.",
keywords = "ACSL, Code analysis, Code generation, Formal specification, Frama-C, Transformation",
author = "Michele Alberti and Julien Signoles",
note = "Publisher Copyright: {\textcopyright} 2018, Springer International Publishing AG, part of Springer Nature.; 27th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2017 ; Conference date: 10-10-2017 Through 12-10-2017",
year = "2018",
month = jan,
day = "1",
doi = "10.1007/978-3-319-94460-9\_6",
language = "English",
isbn = "9783319944593",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "93--111",
editor = "Fabio Fioravanti and Gallagher, \{John P.\}",
booktitle = "Logic-Based Program Synthesis and Transformation - 27th International Symposium, LOPSTR 2017, Revised Selected Papers",
}