CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

The Auspicious Couple: Symbolic Execution and WCET Analysis

Armin Biere ; Jens Knoop ; Laura Kovacs (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Jakob Zwirchmayr
Proceedings of the 13th International Workshop on Worst-Case Execution Time Analysis (WCET 2013), July 9, 2013, Paris, France. Claire Maiza (editor), OASICS Series of Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik Vol. 30 (2013), p. 53-63.
[Konferensbidrag, refereegranskat]

We have recently shown that symbolic execution together with the implicit path enumeration technique can successfully be applied in the Worst-Case Execution Time (WCET) analysis of programs. Symbolic execution offers a precise framework for program analysis and tracks complex program properties by analyzing single program paths in isolation. This path-wise program exploration of symbolic execution is, however, computationally expensive, which often prevents full symbolic analysis of larger applications: the number of paths in a program increases exponentially with the number of conditionals, a situation denoted as the path explosion problem. Therefore, for applying symbolic execution in the timing analysis of programs, we propose to use WCET analysis as a guidance for symbolic execution in order to avoid full symbolic coverage of the program. By focusing only on paths or program fragments that are relevant for WCET analysis, we keep the computational costs of symbolic execution low. Our WCET analysis also profits from the precise results derived via symbolic execution. In this article we describe how use-cases of symbolic execution are materialized in the r-TuBound toolchain and present new applications of WCET-guided symbolic execution for WCET analysis. The new applications of selective symbolic execution are based on reducing the effort of symbolic analysis by focusing only on relevant program fragments. By using partial symbolic program coverage obtained by selective symbolic execution, we improve the WCET analysis and keep the effort for symbolic execution low.

Nyckelord: formal methods, program analysis, program verification, timing analysis, symbolic execution, decision procedures, automated reasoning

Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2014-01-07. Senast ändrad 2016-08-22.
CPL Pubid: 191607


Läs direkt!

Länk till annan sajt (kan kräva inloggning)