Automatic Creation of Environment Models via Training

Abstract. Model checking suffers not only from the state-space explosion problem, but also from the environment modeling problem: how can one create an accurate enough model of the environment to enable precise yet efficient model checking? We present a novel approach to the automatic creation of environment models via training. The idea of training is to take several programs that use a common API and apply model checking to create abstractions of the API proThese abstractions then are reused on subsequent verification runs to model-check different programs (which utilize the same API). This approach has been realized in SLAM, a software model checker for C programs, and applied to the domain of Windows device drivers that utilize the Windows Driver Model API (a set of entry points into the Windows kernel). We show boolean abstractions of the kernel routines accessed from a device driver are extracted and merged into a boolean library that can be reused by subsequent ecking runs on ...

• Type: Conference
• Year: 2004
• Where: TACAS
• Authors: Thomas Ball, Vladimir Levin, Fei Xie
• Keywords: Abstractions, Algorithms, Model Checking, Model Checking Suffers, TACAS 2004