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

Authors Jordy Ruiz, Hugues Cassé

Thumbnail PDF


  • Filesize: 487 kB
  • 10 pages

Document Identifiers

Author Details

Jordy Ruiz
Hugues Cassé

Cite AsGet BibTex

Jordy Ruiz and Hugues Cassé. Using SMT Solving for the Lookup of Infeasible Paths in Binary Programs. In 15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015). Open Access Series in Informatics (OASIcs), Volume 47, pp. 95-104, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


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.
  • WCET
  • infeasible paths
  • SMT
  • machine code


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. C. Barrett, C. Conway, M. Deters, L. Hadarean, D. Jovanovic, T. King, A. Reynolds, and C. Tinelli. CVC4. In 23rd International Conference on Computer Aided Verification (CAV'11), volume 6806 of Lecture Notes in Computer Science. Springer, 2011. Google Scholar
  2. C. Barrett, M. Deters, L. de Moura, A. Oliveras, and A. Stump. 6 Years of SMT-COMP. Journal of Automated Reasoning, 50(3):243-277, 2013. Google Scholar
  3. H. Cassé, F. Birée, and P. Sainrat. Multi-architecture value analysis for machine code. In WCET'13, pages 42-52. OASICs, Dagstuhl Publishing, 2013. Google Scholar
  4. J. Gustafsson, A. Betts, A. Ermedahl, and B. Lisper. The Mälardalen WCET Benchmarks: Past, Present And Future. WCET, 15:136-146, 2010. Google Scholar
  5. J. Henry, M. Asavoae, D. Monniaux, and C. Maïza. How to compute worst-case execution time by optimization modulo theory and a clever encoding of program semantics. SIGPLAN Not., 49(5):43-52, June 2014. Google Scholar
  6. V. Suhendra, T. Mitra, A. Roychoudhury, and Ting C. Efficient detection and exploitation of infeasible paths for software timing analysis. In Design Automation Conference, 2006 43rd ACM/IEEE, pages 358-363, 2006. Google Scholar
  7. N. Williams, B. Marre, P. Mouy, and M. Roger. PathCrawler: Automatic generation of path tests by combining static and dynamic analysis. In Dependable Computing - EDCC 5, volume 3463 of Lecture Notes in Computer Science, pages 281-292. Springer, 2005. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail