CPArec is a tool for verifying recursive C programs via source-to-source program transformation. It uses a recursion-free program analyzer CPAChecker as a black box and computes function summaries from the inductive invariants generated by CPAChecker. Such function summaries enable CPArec to check recursive programs.
Currently this project is unstable. An experimental version CPArec-v0.1-alpha for 2015 Competition on Software Verification is available now.
Python script provided in this project is not directly excutable due to various external tools we use.
Please use our prebuilt release. The following setup is for using the prebuilt release on Ubuntu 12.04 64-bit.
- Java Runtime Environment required for CPAchecker
- Python 2.7 or version above, but please avoid using Python 3 due to compatibility issues
- Python NetworkX package
- Python PyGraphviz package
In Ubuntu 12.04 64-bit use following commands to install required packages:
$ sudo apt-get install openjdk-7-jre python python-networkx python-pygraphviz
Download and extract our release.
To analyze a C program, please type:
$ python <path/to/>CPArec/main.py <path/to/>program.c
CPArec will print verification result on the screen and indicate the directory where proof is stored.
For further usage help, please type:
$ python <path/to/>CPArec/main.py -h
- CPArec-v0.1-alpha is available now.
This project is maintained by Programing Language and Formal Method (PLFM) group in the Institute of Information Science, Academia Sinica, Taiwan.
- Tsai, Ming-Hsien
- Hsieh, Chiao
Further contact information will be available soon.