University of Otago logo. Computer and Information Science Seminars

Seminar Homepage


Dr David Monniaux, CNRS, France


Precise worst-case execution time (WCET) bounding using satisfiability modulo theory (SMT) testing


Owheo 106 - 1:00 pm, Thursday 30 October


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.

About the Speaker:

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.