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. We 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, We make the extracted model adapting to either program-implied or user-defined abstraction level.