Translate One, Analyze Many: Leveraging the Microsoft Intermediate Language and Source Code Transformation for Model Checking | Zendy

Jesse McGeachie | Zendy; Juergen Dingel | Zendy

Open Access

Translate One, Analyze Many: Leveraging the Microsoft Intermediate Language and Source Code Transformation for Model Checking

Author(s) -

Jesse McGeachie,

Juergen Dingel

Publication year - 2007

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2007.02.057

Subject(s) - computer science , programming language , executable , source code , transformation (genetics) , set (abstract data type) , assertion , model transformation , deadlock , software engineering , theoretical computer science , artificial intelligence , biochemistry , chemistry , consistency (knowledge bases) , gene

In this paper we present a source transformation-based framework to support model checking of source code written with languages belonging to Microsoft's .NET platform. The framework includes a set of source transformation rules to guide the transformation, tools to support assertion checking, as well as a tool for the automation of deadlock detection. The framework results in both executable and formally verifiable artifacts. We provide details of the tools in the framework, and evaluate the framework on a few small case studies

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research