Get rid of inline assembly through verification-oriented lifting
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, 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.
Wed 13 Nov
13:40 - 15:20: Papers - Verification and Bug Detection at Cortez 1 Chair(s): Raghavan KomondoorIndian Institute of Science, Bangalore | ||||||||||||||||||||||||||||||||||||||||||
13:40 - 14:00 Talk | Mutation Analysis for Coq Ahmet CelikThe University of Texas at Austin, Karl PalmskogUniversity of Texas at Austin, Marinela ParovicThe University of Texas at Austin, Emilio Jesús Gallego AriasMINES ParisTech, Milos GligoricThe University of Texas at Austin | |||||||||||||||||||||||||||||||||||||||||
14:00 - 14:20 Talk | Verifying Arithmetic in Cryptographic C Programs Jiaxiang LiuShenzhen University, Xiaomu ShiShenzhen University, Ming-Hsien TsaiAcademia Sinica, Taiwan, Bow-Yaw WangAcademia Sinica, Bo-Yin YangAcademia Sinica Pre-print | |||||||||||||||||||||||||||||||||||||||||
14:20 - 14:40 Talk | Model checking embedded control software using OS-in-the-loop CEGAR Pre-print | |||||||||||||||||||||||||||||||||||||||||
14:40 - 15:00 Talk | Get rid of inline assembly through verification-oriented lifting Frédéric RecoulesCEA LIST, Sebastien BardinCEA LIST, Richard BonichonCEA LIST, Laurent MounierUniversité Grenoble Alpes, Marie-Laure PotetUniversité Grenoble Alpes DOI Pre-print | |||||||||||||||||||||||||||||||||||||||||
15:00 - 15:10 Demonstration | VeriAbs : Verification by Abstraction and Test Generation Mohammad AfzalTata Cosultancy Services, A AsiaTata Cosultancy Services, Avriti ChauhanTata Cosultancy Services, Bharti ChimdyalwarTata Consultancy Services, Priyanka DarkeTata Consultancy Services, Advaita DatarTata Consultancy Services Ltd, Shrawan KumarTata Cosultancy Services, R VenkateshTata Research Development and Design Centre | |||||||||||||||||||||||||||||||||||||||||
15:10 - 15:20 Demonstration | SGUARD: A Feature-based Clustering Tool for Effective Spreadsheet Defect Detection Da LiState Key Lab. for Novel Software Tech. and Dept. of Comp. Sci. and Tech., Nanjing University, Nanjing, China, Huiyan WangState Key Lab. for Novel Software Tech. and Dept. of Comp. Sci. and Tech., Nanjing University, Nanjing, China, Chang XuNanjing University, Ruiqing ZhangSearch Tech. Center Asia, Microsoft, Suzhou, China, Shing-Chi CheungDepartment of Computer Science and Engineering, The Hong Kong University of Science and Technology, Xiaoxing MaState Key Lab. for Novel Software Tech. and Dept. of Comp. Sci. and Tech., Nanjing University |