[Club2] Wed. Nov. 10, 14:00: Sascha Böhme

[Alexander Krauss]

Dear all,

Tomorrow, Sascha will give a talk about his summer activities at 
Microsoft Research.


Verifying C: The Right Heap Model Makes a Difference
====================================================
Wed. Nov. 10, 14:00, MI 00.09.055 ("Alan Turing")

Automatic verification of C programs is challenging, especially when
it comes to functional properties: existing systems easily hit the
borders of their underlying automated provers.  One of the major
bottlenecks of those systems is their encoding of the heap.  While
several different encodings are known, there is barely any knowledge
about which heap model is most suitable for the applied automated
provers.  Yet, the right choice can improve performance by at least
one order of magnitude.