English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

In systems with hard real-time constraints, it is necessary to compute upperbounds on the worst-case execution time (WCET) of programs; the closer thebound to the real WCET, the better. This is especially the case of synchronousreactive control loops with a fixed clock; the WCET of the loop body must notexceed the clock period. We compute the WCET (or at least a close upper boundthereof) as the solution of an optimization modulo theory problem that takesinto account the semantics of the program, in contrast to other methods thatcompute the longest path whether or not it is feasible according to thesesemantics. Optimization modulo theory extends satisfiability modulo theory(SMT) to maximization problems. Immediate encodings of WCET problems into SMTyield formulas intractable for all current production-grade solvers; this isinherent to the DPLL(T) approach to SMT implemented in these solvers. Byconjoining some appropriate "cuts" to these formulas, we considerably reducethe computation time of the SMT-solver. We experimented our approach on avariety of control programs, using the OTAWA analyzer both as baseline and asunderlying microarchitectural analysis for our analysis, and show notableimprovement on the WCET bound on a variety of benchmarks and control programs.

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