Beyer, DirkHenzinger, Thomas A.Théoduloz, Grégory2008-10-302008-10-302008-10-30200810.1109/ASE.2008.13https://infoscience.epfl.ch/handle/20.500.14299/30549We present and evaluate a framework and tool for combining multiple program analyses which allows the dynamic (on-line) adjustment of the precision of each analysis depending on the accumulated results. For example, the explicit tracking of the values of a variable may be switched off in favor of a predicate abstraction when and where the number of different variable values that have been encountered has exceeded a specified threshold. The method is evaluated on verifying the SSH client/server software and shows significant gains compared with predicate abstraction-based model checking.text::conference output::conference proceedings::conference paper