Name
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 rendering state-of-the-art formal analyzers developed for C ineffective. We thus propose TInA, the first automated, generic, verification-friendly and trustworthy lifting technique turning inline assembly into semantically equivalent C code amenable to verification, in order to take advantage of existing C analyzers. Extensive experiments on real-world code (including GMP and ffmpeg) show the feasibility and benefits of TInA.
|
Year | DOI | Venue |
|---|---|---|
2019 | 10.1109/ASE.2019.00060 | ASE |
Keywords | Field | DocType |
Inline assembly, software verification, lifting, formal methods | Embedded software,Software engineering,Systems engineering,Computer science,Inline assembler,Semantic equivalence,Software,Formal methods,Rendering (computer graphics),Software development,Software verification | Conference |
ISSN | ISBN | Citations |
1938-4300 | 978-1-7281-2508-4 | 1 |
PageRank | References | Authors |
0.35 | 0 | 5 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Frédéric Recoules | 1 | 1 | 0.35 |
| Sébastien Bardin | 2 | 297 | 19.35 |
| Richard Bonichon | 3 | 6 | 2.17 |
| Laurent Mounier | 4 | 1187 | 79.54 |
| Marie-Laure Potet | 5 | 190 | 21.34 |