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


Published in:
Proceedings ot the 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2008), 29-38
Presented at:
Automated Software Engineering, L'Aquila, Italy, 15-19 September 2008
Year:
2008
Publisher:
IEEE
Laboratories:




 Record created 2008-10-30, last modified 2018-09-13


Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)