David Monniaux, Verimag<\/p>\n
R\u00e9sum\u00e9:<\/strong><\/p>\n \nIn order to bound the worst case execution time of loop-free programs,why can’t we use standard bounded model checking techniques, on programs adorned with a supplementary “time” counter? The reason is that the logical formulas generated have exponential-size proofs in the proof system used by DPLL(T) SMT-solvers, thus all current stable SMT-solvers; thus this approach is intractable. In this talk we explain how to work wound this difficulty by adding Joint work with Julien Henry, Claire Maiza, Diego Caminha\n<\/p><\/blockquote>\n <\/p>\n","protected":false},"excerpt":{"rendered":" Death by a thousand cuts (worst-case execution time by bounded model checking) !!! report\u00e9 au : Friday, 29 nov 2013, LIP, 13H30, Salle du Conseil David Monniaux, Verimag R\u00e9sum\u00e9: In order to bound the worst case execution time of loop-free … Continue reading
\nsupplementary, redundant constraints (“cuts”) to the formula, in order to kill its complexity. <\/p>\n