itee seminar: Dr Tim Menzies, 02.00PM, Thu 11 Dec 2003

On the Advantages of Approximate vs. Complete Verification: Bigger Models, Faster, Less Memory, Usually Accurate

Speaker: Dr Tim Menzies, NASA Independent Verification and Validation Facility

When: 02.00PM, Thursday 11 Dec 2003

Venue: 78-420

Host: Peter Lindsay

Abstract:

  As software grows increasingly complex, verification becomes more
  and more challenging.  Automatic verification by model checking has
  been effective in many domains . However, Many real world software
  models, however, are too large for the available tools.

  We have been exploring LURCH, an approximate (not necessarily
  complete) alternative to traditional model checking based on a
  randomized search algorithm.

  The cost of randomized algorithms are their inaccuracies.  If
  complete algorithms terminate, they find all the features they are
  searching for. On the other hand, by their very nature, randomized
  algorithms can miss important features. Our experiments suggest that
  this inaccuracy problem is not too serious. In the case studies
  presented here LURCH’s random search usually found the correct
  results.

  Also, these case studies strongly suggest that LURCH can scale to
  much larger models than standard model checkers like NuSMV and SPIN.

Biography:

  Tim's all right: none too bright but can lift heavy things. PhD
  grad from UNSW (AI), 1995.  Refugee from the expert systems bubble
  bursting in the early 1990s. Ran away to American these last five
  years to work with NASA. Says that Dave Carrington and Bob Colomb
  had a huge impact on his career. Does not say if that impact was for
  better or for worse.  For more on the speaker, see his web site
  (http://menzies.us), his bio (http://menzies.us/me.html) or his 150+
  publications (http://menzies.us/papers.html). His latest publication
  "Data Mining for Very Busy People" appeared in IEEE Computer,
  November 2003.

Contact:

Peter Lindsay, seminar host (Peter.Lindsay@itee.uq.edu.au)
or Guido Governatori (ITEE seminar co-ordinator) (guido@itee.uq.edu.au)

ITEE seminar web page: http://www.itee.uq.edu.au/~seminar

[All seminars]