Welcome to Ke Jiang's Homepage

C to Promela translator

Here is the sorce code - primary version (lastest update: 2009/08/11) of my MSc thesis project "Model Checking C programs by Translating C to Promela". If you are using, will use this program or find bugs, please drop me a mail. :-) The program will be updated from time to time until late 2009.

Installation instructions

1. System requirements:

• GNU make
• OCaml 3.08 or higher. You can get the latest OCaml from http://caml.inria.fr/ocaml/

2. Installation

• Uncompress the distribution
• cd into the directory:

  $ cd C2Promela

• Configure:

  $ ./configure

• Make:

  $ make

3. Usage

• To translate all the example C codes user ./examples:

  Run ./examples/doexamples

• To translate a self-defined C code which satisfies the syntax limits.

  Run ./doc2p sourcefile targetfile

  e.g. $ ./doc2p /home/jacky/test.c /home/jacky/test.pml

Publication

• Using SPIN to Model Check Concurrent Algorithms, using a translation from C to Promela
  Ke Jiang, Bengt Jonsson
  In Second Swedish Workshop on Multi-Core Computing (MCC09), 2009. pdf version

For more information about me or the project, please contact me by Email: ke.jiang (at) liu (dot) se.