Obavijest o predavanju

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/