Program Analysis with Dynamic Precision Adjustment

Dirk Beyer, Thomas A. Henzinger, Grégory Théoduloz

Full text DOI 10.1109/ase.2008.13 dblp

Abstract

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 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.

BibTeX

@inproceedings{Beyer-al:ASE08,
  author    = {Dirk Beyer and
               Thomas A. Henzinger and
               Gr{\'{e}}gory Th{\'{e}}oduloz},
  title     = {Program Analysis with Dynamic Precision Adjustment},
  booktitle = {ASE},
  pages     = {29--38},
  publisher = {{IEEE} Computer Society},
  year      = {2008},
}

Program Analysis with Dynamic Precision Adjustment

Abstract

Related papers