Automatic Verification of Strongly Dynamic Software Systems
N. Dor, J. Field, D. Gopan, T. Lev-Ami, A. Loginov, R. Manevich,
G. Ramalingam, T. Reps, N. Rinetzky, M. Sagiv, R. Wilhelm,
E. Yahav, and G. Yorsh
Strongly dynamic software systems are difficult to verify.
By strongly dynamic, we mean that the actors in such systems
change dynamically, that the resources used by such systems are
dynamically allocated and deallocated, and that for both sets, no
bounds are statically known.
In this position paper, we describe the progress we have made in
automated verification of strongly dynamic systems using abstract
interpretation with three-valued logical structures. We then
enumerate a number of challenges that must be tackled in order for
such techniques to be widely adopted.
(Click here to access the paper:
PostScript,
PDF.)