Boosting Verification by Automatic Tuning of Decision Procedures

Add to your list(s) Download to your calendar using vCal

• Domagoj Babic (University of British Columbia)
• Tuesday 18 September 2007, 13:00-14:00
• Computer Laboratory, William Gates Building, Room SS03.

If you have a question about this talk, please contact Thomas Tuerk.

Parameterized heuristics abound in computer aided-design and verification, and manual tuning of the respective parameters is difficult and time-consuming. Very recent results from the artificial intelligence (AI) community suggest that this tuning process can be automated, and that doing so can lead to significant performance improvements; furthermore, automated parameter optimization can provide valuable guidance during the development of heuristic algorithms. Such an AI approach can improve a state-of-the-art SAT solver for large, real-world bounded model-checking and software verification instances. The resulting, automatically-derived parameter settings yielded runtimes on average 4.5 times faster on bounded model checking instances and 500 times faster on software verification problems than extensive hand-tuning of the decision procedure. Furthermore, the availability of automatic tuning influenced the design of the solver, and the automatically-derived parameter settings provided a deeper insight into the properties of problem instances.

Domagoj Babic´s Homepage: http://www.domagoj.info

This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Computer Laboratory Automated Reasoning Group Lunches
• Computer Laboratory talks
• Computer Laboratory, William Gates Building, Room SS03
• School of Technology

Note that ex-directory lists are not shown.