How to Compute Worst-Case Execution Time by Optimization Modulo Theory and a Clever Encoding of Program Semantics

Julien Henry, Mihail Asavoae, David Monniaux +1

In systems with hard real-time constraints, it is necessary to compute upper bounds on the worst-case execution time (WCET) of programs; the closer the bound to the real WCET, the…