Abstract | ||
---|---|---|
Formal methods for software development have made great strides in the last two decades, to the point that their application in safety-critical embedded software is an undeniable success. Their extension to non-critical software is one of the notable forthcoming challenges. For example, C programmers regularly use inline assembly for low-level optimizations and system primitives. This usually results in driving state-of-the-art formal analyzers developed for C ineffective. We thus propose TInA, an automated, generic, trustable and verification-oriented lifting technique turning inline assembly into semantically equivalent C code, in order to take advantage of existing C analyzers. Extensive experiments on real-world C code with inline assembly (including GMP and ffmpeg) show the feasibility and benefits of TInA. |
Year | Venue | DocType |
---|---|---|
2019 | CoRR | Journal |
Volume | Citations | PageRank |
abs/1903.06407 | 0 | 0.34 |
References | Authors | |
0 | 5 |
Name | Order | Citations | PageRank |
---|---|---|---|
Frédéric Recoules | 1 | 0 | 0.34 |
Sébastien Bardin | 2 | 30 | 4.88 |
Richard Bonichon | 3 | 87 | 6.91 |
Laurent Mounier | 4 | 1187 | 79.54 |
Marie-Laure Potet | 5 | 0 | 0.34 |