english only
EPFL > I&C > Tresor > Seminars
Research Topics
Useful Links


This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
seminars [2013/07/10 17:24]
seminars [2013/07/10 18:26]
Line 14: Line 14:
 \\ \\
-====== ​Upcoming ​Talks ======+====== ​Recent Notable ​Talks ======
 \\ \\
 +===== Bounded Model-Checking for Worst-Case Execution Time =====
 +  * 2013-06-06 - 11:30, [[http://​plan.epfl.ch/?​lang=en&​room=BC410|BC 410]], [[http://​www-verimag.imag.fr/​~monniaux|David Monniaux]], VERIMAG, France
 +In real-time critical applications (e.g. automotive, aerospace), it is
 +necessary to guarantee that the body of control loops execute within
 +certain time bounds. The problem of finding the worst case execution
 +time of a program, or at least bounding it reasonably tightly, is hard
 +for two reasons: (1), current architectures are very complex, with
 +caches, shared components and pipelines, and using methods valid 25
 +years ago (take the worst-case time of each instruction and sum) would
 +lead to gross overapproximation;​ (2), even if a path in the code is
 +syntactically feasible, it is not necessarily so if taking into account
 +the semantics of the program (e.g. two blocks of code apply to two
 +disjoint modes of operation of the system and cannot be executed both in
 +a single iteration).
 +One alluring idea is to use bounded model-checking by SMT-solving to
 +determine the worst-case execution time (which takes care of (2) and
 +even (1)). Doing so naively is however prohibitively expensive; we have
 +experimental results and theoretical explanations for this. We provide a
 +solution to this problem, based on local abstractions.
 ===== Roles of Types in Logic, Computation and Security - an Overview ===== ===== Roles of Types in Logic, Computation and Security - an Overview =====