Death by a thousand cuts
(worst-case execution time by bounded model checking)

!!! reporté au : Friday, 29 nov 2013, LIP, 13H30, Salle du Conseil

David Monniaux, Verimag

Résumé:

In 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
supplementary, redundant constraints (“cuts”) to the formula, in order to kill its complexity.

Joint work with Julien Henry, Claire Maiza, Diego Caminha