@inproceedings{b85c60c3a8d74113b20bab6be0371c19,
title = "Common specification language for static and dynamic analysis of C programs",
abstract = "Various combinations of static and dynamic analysis techniques were recently shown to be beneficial for software verification. A frequent obstacle to combining different tools in a completely automatic way is the lack of a common specification language. Our work proposes to translate a Pre-Post based specification into executable C code. This paper presents E-ACSL, subset of the ACSL specification language for C programs, and its automatic translator into C implemented as a FRAMA-C plug-in. The resulting C code is executable and can be used by a dynamic analysis tool. We illustrate how the PATHCRAWLER test generation tool automatically treats such pre- and postconditions specified as C functions.",
author = "Micka{\"e}l Delahaye and Nikolai Kosmatov and Julien Signoles",
year = "2013",
month = jan,
day = "1",
doi = "10.1145/2480362.2480593",
language = "English",
isbn = "9781450316569",
series = "Proceedings of the ACM Symposium on Applied Computing",
publisher = "Association for Computing Machinery",
pages = "1230--1235",
booktitle = "28th Annual ACM Symposium on Applied Computing, SAC 2013",
note = "28th Annual ACM Symposium on Applied Computing, SAC 2013 ; Conference date: 18-03-2013 Through 22-03-2013",
}