Vous pouvez vous abonner à nos annonces de séminaires
		    http://gallium.inria.fr/seminaires/

			     S E M I N A I R E
			   __
			  / _`  _   /  /  o
			 /   ) __) /  /  / /  / /\/|
			(___/ (_/ (_ (_ / (__/ /   |

			     I N R I A - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                          Salle Lions 2, bâtiment C

                           Lundi 11 juillet, 10h30

                             -------------------
                             Clément Pit-Claudel
                             -------------------

                                     MIT

         ===========================================================
         Trigger Selection Strategies to Stabilize Program Verifiers
         ===========================================================

SMT-based program verifiers often suffer from the so-called butterfly effect,
in which minor modifications to the program source cause significant
instabilities in verification times, which in turn may lead to spurious
verification failures and a degraded user experience. This paper identifies
matching loops (ill-behaved quantifiers causing an SMT solver to repeatedly
instantiate a small set of quantified formulas) as a significant contributor
to these instabilities, and describes some techniques to detect and prevent
them. At their core, the contributed techniques move the trigger selection
logic away from the SMT solver and into the high-level verifier: this move
allows authors of verifiers to annotate, rewrite, and analyze user-written
quantifiers to improve the solver's performance, using information that is
easily available at the source level but would be hard to extract from the
heavily encoded terms that the solver works with. The paper demonstrates three
core techniques (quantifier splitting, trigger sharing, and matching loop
detection) by extending the Dafny verifier with its own trigger selection
routine, and demonstrates significant predictability and performance gains on
both Dafny's test suite and large verification efforts using Dafny.

(Joint work with K. Rustan M. Leino.)