Developing automated
techniques for validating/verifying software - at
compile-time, run-time or post-mortem- is of obvious
importance. Such techniques are vital for program
understanding and reliable program development. There is
renewed interest in automated software validation due to
recent progress in automatic extraction of transition
system-like models from code. This makes model checking
-- a search-based automated verification technique for
hardware circuits/microprocessors -- accessible for
software verification as well. Currently, there is lot
of work in both academia and industry in using model
checking for debugging realistic pieces of software such
as device drivers. This project will investigate a
related but somewhat different theme: integration of
search-based debugging methods into (embedded) software
development. We do not directly use model checking for
debugging. However, search-based simulation/checking
methods are used to increase the degree of automation in
existing debugging tasks.
Our focus is mostly on
embedded/control systems and we are working both at the
requirements (model) level as well as the program level.
The specific research directions being pursued are as
follows.