Kratak sadržaj predavanja

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 decision procedure

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 prover,

and the automatically-derived parameter settings provided a deeper

insight into the properties of problem instances.

Paper available at: http://www.cs.ubc.ca/~babic/papers/fmcad07.pdf

O predavaču

Domagoj Babic is a Ph.D. candidate at the University of British

Columbia. His research interests include software verification and

analysis, as well as automated theorem proving and SAT solving.

Domagoj is currently working on a scalable and precise static checker

Calysto, and a bit-vector decision procedure Spear for software

verification. He is planning to graduate in early spring 2008.

Domagoj holds a M.Sc. degree in computer science and a Dipl.Ing.

degree in industrial electronics from the Faculty of Electrical

Engineering and Computing at Zagreb University. Domagoj is a

Microsoft Fellow (2005-2007).

For more information, see http://www.domagoj.info/