Model Checking C# Code: A Translation Approach
Extracting model from source code helps to ensure the implementation in accord with design. The properties of interest can be checked on implemented system via the extracted model. Previous approaches usually abstract the source at the level of intermediate language or assembly code. The authors are building a module to automatically extract CSP# model from C# source code and use PAT (Process Analysis Toolkit) to check the properties. As PAT support user-defined C# data type, they make the extracted model adapting to either program-implied or user-defined abstraction level.