Redesigning NIPS VM as a Symbolic Execution Engine
NIPS is an umbrella project for several model checking components:
- A virtual machine (VM) specification and implementation (in form of
a library) with the expressed aim to act as a state space generator for
model checking purposes, and to be easily embeddable into third-party
tools.
- A compiler for the Promela language which targets the virtual
instruction set of the NipsVM, thus providing an alternative way to
verify models written for the SPIN model checking tool.
- The compiler of the MCESS framework targets NipsVM, thus providing
a route to verify C and assembly code for several micro-controllers
via model checking.
- The SARN framework provides several static analyses and state space
reductions which work on NipsVM byte-code, to a large degree
regardless of the actual source language.
All of these components have in common that they are carrying out
control or data-flow analyses for optimization and other purposes.
The interface between them is effectively the semantics of the
byte-code language, duplicated among all the tools.
The aim of this project is to use the insights gained with the
existing implementation for a redesign, which removes the duplication
of functionality, and extends NipsVM with an option to execute
byte-code symbolically, thus allowing control and data-flow
analyses to reuse the VM.
Literature