Classically, worst-case execution time is bounded using 1) a low-level analysis of caches, pipelines etc. producing a worst-case execution time for each control block; 2) a reassembly phase, producing the worst-case execution time for the whole program, most often by integer linear programming. This second phase may unfortunately take into account paths that are in reality infeasible due to conflicting conditions, resulting in an an over-estimation of the WCET.
In this work we propose an approach for WCET for loop-free programs, typically the loop bodies of embedded control applications, based on satisfiability modulo theory (SMT) testing. We discuss the difficulties with a too naive encoding of the problem into SMT, workarounds, and practical performance.
This is joint work with Julien Henry, Mihail Asavoae and Claire Maiza, presented at ACM LCTES 2014.
David Monniaux is senior researcher at CNRS, VERIMAG laboratory, Grenoble, France, and part-time associate professor at Ecole polytechnique, Paris. He works broadly in formal methods, on the static analysis of programs, and on the algorithmics of decision procedures and static analysis.
He is visiting the Computer Science until December 15 and is in office 248.
Last modified: Tuesday, 28-Oct-2014 08:13:15 NZDT
This page is maintained by the seminar list administrator.