english only
EPFL > I&C > Tresor > Seminars
RESOURCES
Home
People
Seminars
Courses
Research Topics
Events
Useful Links

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
seminars [2013/07/10 17:15]
gvero
seminars [2017/06/28 18:20] (current)
Line 7: Line 7:
  
   * Past talks: [[seminars:​2010|2010]],​ [[seminars:​2009|2009]],​ [[seminars:​2008|2008]],​ [[seminars:​2007|2007]],​ [[seminars:​2006|2006]],​ [[seminars:​2005|2005]]   * Past talks: [[seminars:​2010|2010]],​ [[seminars:​2009|2009]],​ [[seminars:​2008|2008]],​ [[seminars:​2007|2007]],​ [[seminars:​2006|2006]],​ [[seminars:​2005|2005]]
-  * [[:​seminars:​calendar|Graphical Calendar]] 
-  * [[:​seminars:​MeetingRoom|Reserve Tresor Conference Room BC355]] 
   * [[:​seminars:​Instructions|Instructions]]   * [[:​seminars:​Instructions|Instructions]]
  
 +\\
 \\ \\
  
-====== ​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
 +
 +Abstract:
 +
 +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 logiccomputation ​and security ​- an overview ​=====+===== Roles of Types in LogicComputation ​and Security ​- an Overview ​=====
  
   * 2013-02-28 - 15:00, [[http://​plan.epfl.ch/?​lang=en&​room=BC410|BC 410]], [[http://​imft.ftn.uns.ac.rs/​~silvia|Prof. Silvia Ghilezan]], University of Novi Sad, Serbia   * 2013-02-28 - 15:00, [[http://​plan.epfl.ch/?​lang=en&​room=BC410|BC 410]], [[http://​imft.ftn.uns.ac.rs/​~silvia|Prof. Silvia Ghilezan]], University of Novi Sad, Serbia
Line 25: Line 49:
 I will present an overview of results that emerged from type theoretic techniques. A particular attention will be given to the reducibility method in logic. Further, the role of classical types will be presented in the framework of delimited continuations. Finally, the role of types will be discussed in security control issues of linked documents and linked data. I will present an overview of results that emerged from type theoretic techniques. A particular attention will be given to the reducibility method in logic. Further, the role of classical types will be presented in the framework of delimited continuations. Finally, the role of types will be discussed in security control issues of linked documents and linked data.
  
-\\ 
 \\ \\
 ===== Transformation-based Program Analysis and Logic Solvers ===== ===== Transformation-based Program Analysis and Logic Solvers =====
Line 35: Line 58:
 Word level compilers and linkers apply transformations at the word level to generate smaller and faster programs. Several techniques at the Boolean and circuit levels effectively reduce the complexity and the size of the program and make it amenable to decision procedures such as satisfiability solvers. These techniques miss many opportunities of optimizations that exist at the word level. Transformations such as word based compositional minimization,​ and word based abstractions are not even possible at the Boolean or circuit levels. ​ Word level compilers and linkers apply transformations at the word level to generate smaller and faster programs. Several techniques at the Boolean and circuit levels effectively reduce the complexity and the size of the program and make it amenable to decision procedures such as satisfiability solvers. These techniques miss many opportunities of optimizations that exist at the word level. Transformations such as word based compositional minimization,​ and word based abstractions are not even possible at the Boolean or circuit levels. ​
 In this talk we consider several techniques for program analysis including word level transformation based analysis. In this talk we consider several techniques for program analysis including word level transformation based analysis.
 +