This work has been supported by the NSF grant CCF-0950678
This
work has been supported by the NSF grant CCF-0950678
Permission to use, copy, modify, and distribute this software and its documentation for NON-COMMERCIAL purposes and without fee is hereby granted provided that this copyright notice appears in all copies. Use UPC-ModEx at your own risk. Michigan Technological University and Ali Ebnenasir SHALL NOT BE LIABLE FOR ANY DAMAGES SUFFERED BY THE USERS AS A RESULT OF USING, MODIFYING OR DISTRIBUTING THIS SOFTWARE.
UPC-ModEx is an extension of the ANSI C Model Extractor (ModEx) that supports the UPC grammar and enables the extraction of Promela models from UPC programs.
UPC Model Extractor (UPC-ModEx) -
binary executable on MS-Windows
Case Studies:
1) Integer Permutation:
- Original
UPC source code
- Sliced
UPC source code
- Abstraction
Look-Up Table (LUT)
- Promela
model
- Properties
of interest
- Results
of verification
2) Heat Flow:
- Original UPC
source code
- Sliced
UPC source code
- Abstraction
Look-Up Table (LUT)
- Promela
model
- Properties
of interest
- Results
of verification
3) Bubble sort:
- Original
UPC source code
- Sliced
UPC source code
- Abstraction
Look-Up Table (LUT)
- Promela
model
- Properties
of interest
- Results
of verification
4) Parallel Data
Collection:
- Original
UPC source code
- Sliced
UPC source code
- Abstraction
Look-Up Table (LUT)
- Promela
model
- Properties
of interest
- Results
of verification
5) Conjugate Gradient
(CG) kernel of NASA's Narallel Benchmark (NPB)
- Original
UPC source code
- Sliced
UPC source code
- Abstraction
Look-Up Table (LUT)
- Promela
model
- Properties
of interest
- Results
of verification