Program Analysis with Dynamic Precision Adjustment

We 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 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 ion-based model checking.

• Type: Conference
• Year: 2008
• Where: KBSE
• Authors: Dirk Beyer, Thomas A. Henzinger, Grégory Théoduloz
• Keywords: KBSE 2008, Multiple Program Analyses, Predicate Abstraction, Predicate Ion-based Model, Software Engineering