OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Using SMT Solving for the Lookup of Infeasible Paths in Binary Programs

Ruiz, Jordy and Cassé, Hugues Using SMT Solving for the Lookup of Infeasible Paths in Binary Programs. (2015) In: 15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015), 7 July 2015 (Lund, Sweden).

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL: http://dx.doi.org/10.4230/OASIcs.WCET.2015.95


Worst-Case Execution Time (WCET) is a key component to check temporal constraints of realtime systems. WCET by static analysis provides a safe upper bound. While hardware modelling is now efficient, loss of precision stems mainly in the inclusion of infeasible execution paths in the WCET calculation. This paper proposes a new method to detect such paths based on static analysis of machine code and the feasibility test of conditions using Satisfiability Modulo Theory (SMT) solvers. The experimentation shows promising results although the expected precision was slightly lowered due to clamping operations needed to cope with complexity explosion. An important point is that the implementation has been performed in the OTAWA framework and is independent of any instruction set thanks to its semantic instructions.

Item Type:Conference or Workshop Item (Paper)
Additional Information:Thanks to Dagstuhl Research Online Publication Server (DROPS)Distribution of this paper is permitted under the terms of the Creative Commons license CC-by-nc-nd 4.0. This paper appears inOpenAccess Series in Informatics (OASIcs)ISBN 978-3-939897-95-8 ISSN 2190-6807 The definitive version is available at: http://drops.dagstuhl.de/opus/volltexte/2015/5260/
HAL Id:hal-01371783
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE)
French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Laboratory name:
Deposited On:07 Sep 2016 12:37

Repository Staff Only: item control page